awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₁ : n ∈ S
⊢ Membership.mem (γ := Set B) ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) x
have refine_1 : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
x : B
n : ℕ
hnpow : n ≠ 0 ∧ x ^ n = 1
hn₂ : n ∈ T
⊢ Membership.mem (γ := Set B) ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) x
have refine_1 : Membership.mem (γ := Set B) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1} x
Tactic: right
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
⊢ IsCyclotomicExtension T (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B
have this : Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
  ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
Tactic: have : {b : B | ∃ n : ℕ, n ∈ S ∪ T ∧ n ≠ 0 ∧ b ^ n = 1} =
      {b : B | ∃ n : ℕ, n ∈ S ∧ n ≠ 0 ∧ b ^ n = 1} ∪
        {b : B | ∃ n : ℕ, n ∈ T ∧ n ≠ 0 ∧ b ^ n = 1} := by
    refine le_antisymm ?_ ?_
    · rintro x ⟨n, hn₁ | hn₂, hnpow⟩
      · left; exact ⟨n, hn₁, hnpow⟩
      · right; exact ⟨n, hn₂, hnpow⟩
    · rintro x (⟨n, hn⟩ | ⟨n, hn⟩)
      · exact ⟨n, Or.inl hn.1, hn.2⟩
      · exact ⟨n, Or.inr hn.1, hn.2⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
⊢ IsCyclotomicExtension T (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B
have refine : ∀ (b : B),
  Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
Tactic: refine ⟨fun hn => ((isCyclotomicExtension_iff _ A _).1 h).1 (mem_union_right S hn), fun b => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
b : B
⊢ Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
have h₁ : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) b
Tactic: replace h := ((isCyclotomicExtension_iff _ _ _).1 h).2 b
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
b : B
h : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) b
⊢ Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
have rwa : ∀
  (h :
    Membership.mem (γ := Subalgebra A B)
      (adjoin A ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})) b),
  Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
Tactic: rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
b : B
h : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) b
rwa :
  ∀
    (h :
      Membership.mem (γ := Subalgebra A B)
        (adjoin A ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})) b),
    Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
      (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
⊢ Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
have rwa₁ : ∀
  (h :
    Membership.mem (γ := Subalgebra A B)
      (Subalgebra.restrictScalars A (S := ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
        (adjoin ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}))
      b),
  Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
Tactic: rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
this :
  Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
b : B
h : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) b
rwa :
  ∀
    (h :
      Membership.mem (γ := Subalgebra A B)
        (adjoin A ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})) b),
    Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
      (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
rwa₁ :
  ∀
    (h :
      Membership.mem (γ := Subalgebra A B)
        (Subalgebra.restrictScalars A (S := ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
          (adjoin ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}))
        b),
    Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
      (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
⊢ Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
have rwa₂ : ∀
  (h :
    Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) B)
      (adjoin ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b),
  Membership.mem (γ := Subalgebra (↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) B)
    (adjoin ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1}) b
Tactic: rwa [this, adjoin_union_eq_adjoin_adjoin, Subalgebra.mem_restrictScalars] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
⊢ IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
have refine_1 : ∀ {n : ℕ} (hn : n ∈ S) (hn' : n ≠ 0), ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n
Tactic: refine ⟨fun {n} hn hn' => ?_, fun b => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
refine_1 :
  ∀ {n : ℕ} (hn : n ∈ S) (hn' : n ≠ 0), ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n
⊢ IsCyclotomicExtension.{u, v} S A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
have refine_2 : ∀ (b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})),
  Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) b
Tactic: refine ⟨fun {n} hn hn' => ?_, fun b => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ
hn : n ∈ S
hn' : n ≠ 0
⊢ ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n
have refine_1 : ∀ (b : B) (hb : IsPrimitiveRoot b n), ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n
Tactic: obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 h).1 (hS hn) hn'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ
hn : n ∈ S
hn' : n ≠ 0
b : B
hb : IsPrimitiveRoot b n
⊢ ∃ (r : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})), IsPrimitiveRoot r n
have refine_1 : IsPrimitiveRoot (M := ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
  (Subtype.mk (p := fun (x : B) ↦
    Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) x) b sorry)
  n
Tactic: refine ⟨⟨b, subset_adjoin ⟨n, hn, hn', hb.pow_eq_one⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
n : ℕ
hn : n ∈ S
hn' : n ≠ 0
b : B
hb : IsPrimitiveRoot b n
⊢ IsPrimitiveRoot (M := ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) x) b ⋯)
    n
have refine_1 : IsPrimitiveRoot
  (↑(Subtype.mk (p := fun (x : B) ↦
        Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) x) b sorry) :
    B)
  n
Tactic: rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) b
have h₁ : Eq.{v + 1} (α := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
  (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤
Tactic: convert! mem_top (R := A) (x := b)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ Eq.{v + 1} (α := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤
have h₁ : Eq.{v + 1} (α := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
  (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
  (adjoin A {a : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ a_1 ∈ S, a_1 ≠ 0 ∧ (↑a : B) ^ a_1 = 1})
Tactic: rw [← adjoin_adjoin_coe_preimage, preimage_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension T A B
hS : S ⊆ T
b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})
⊢ Eq.{v + 1} (α := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (adjoin A {a : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ a_1 ∈ S, a_1 ≠ 0 ∧ (↑a : B) ^ a_1 = 1})
have h₁ : Eq.{v + 1} (α := Subalgebra A ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
  (adjoin A {b : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ n ∈ S, ¬n = 0 ∧ b ^ n = 1})
  (adjoin A {a : ↥(adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) | ∃ a_1 ∈ S, ¬a_1 = 0 ∧ a ^ a_1 = 1})
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
⊢ IsCyclotomicExtension (S ∪ {n}) A B
have pos : ∀ (hn : n = 0), IsCyclotomicExtension (S ∪ {n}) A B
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
pos : ∀ (hn : n = 0), IsCyclotomicExtension (S ∪ {n}) A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B
have neg : ∀ (hn : ¬n = 0), IsCyclotomicExtension (S ∪ {n}) A B
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
⊢ IsCyclotomicExtension (S ∪ {n}) A B
have pos : IsCyclotomicExtension (S ∪ {0}) A B
Tactic: rwa [hn, eq_self_sdiff_zero, Set.union_diff_right, ← eq_self_sdiff_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
pos : IsCyclotomicExtension (S ∪ {0}) A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B
have pos₁ : IsCyclotomicExtension ((S ∪ {0}) \ {0}) A B
Tactic: rwa [hn, eq_self_sdiff_zero, Set.union_diff_right, ← eq_self_sdiff_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : n = 0
pos : IsCyclotomicExtension (S ∪ {0}) A B
pos₁ : IsCyclotomicExtension ((S ∪ {0}) \ {0}) A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B
have pos₂ : IsCyclotomicExtension (S \ {0}) A B
Tactic: rwa [hn, eq_self_sdiff_zero, Set.union_diff_right, ← eq_self_sdiff_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ IsCyclotomicExtension (S ∪ {n}) A B
have neg : (∀ n_1 ∈ S ∪ {n}, n_1 ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n_1) ∧
  Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤
Tactic: rw [iff_adjoin_eq_top]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ (∀ n_1 ∈ S ∪ {n}, n_1 ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n_1) ∧
    Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤
have neg : ∀ (m : ℕ) (hm₁ : m ∈ S ∪ {n}) (hm₂ : m ≠ 0), ∃ (r : B), IsPrimitiveRoot r m
Tactic: refine ⟨fun m hm₁ hm₂ ↦ ?_, le_antisymm (by simp) ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
neg : ∀ (m : ℕ) (hm₁ : m ∈ S ∪ {n}) (hm₂ : m ≠ 0), ∃ (r : B), IsPrimitiveRoot r m
⊢ (∀ n_1 ∈ S ∪ {n}, n_1 ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n_1) ∧
    Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤
have neg₁ : LE.le.{v} (α := Subalgebra A B) ⊤ (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
Tactic: refine ⟨fun m hm₁ hm₂ ↦ ?_, le_antisymm (by simp) ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
m : ℕ
hm₁ : m ∈ S ∪ {n}
hm₂ : m ≠ 0
⊢ ∃ (r : B), IsPrimitiveRoot r m
have neg : ∀ (hm₁ : m ∈ S), ∃ (r : B), IsPrimitiveRoot r m
Tactic: obtain hm₁ | rfl := hm₁
Cleared hypotheses: hm₁
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
m : ℕ
hm₁ : m ∈ S ∪ {n}
hm₂ : m ≠ 0
neg : ∀ (hm₁ : m ∈ S), ∃ (r : B), IsPrimitiveRoot r m
⊢ ∃ (r : B), IsPrimitiveRoot r m
have neg₁ : ∀ [NeZero m] (hr : IsPrimitiveRoot r m) (hn : ¬m = 0), ∃ (r : B), IsPrimitiveRoot r m
Tactic: obtain hm₁ | rfl := hm₁
Cleared hypotheses: n, inst, hr, hn, hm₁
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
hB : IsCyclotomicExtension S A B
r : B
hr : IsPrimitiveRoot r n
hn : ¬n = 0
⊢ LE.le.{v} (α := Subalgebra A B) ⊤ (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
have neg : LE.le.{v} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
  (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1})
Tactic: rw [← ((iff_adjoin_eq_top _ _ _).mp hB).2]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
⊢ IsCyclotomicExtension (S ∪ {n}) A B
have refine_1 : ∀ (s : ℕ) (hs : s ∈ S ∪ {n}) (hs' : s ≠ 0), ∃ (r : B), IsPrimitiveRoot r s
Tactic: refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs hs' ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
refine_1 : ∀ (s : ℕ) (hs : s ∈ S ∪ {n}) (hs' : s ≠ 0), ∃ (r : B), IsPrimitiveRoot r s
⊢ IsCyclotomicExtension (S ∪ {n}) A B
have refine_2 : Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n_1 ∈ S ∪ {n}, n_1 ≠ 0 ∧ b ^ n_1 = 1}) ⊤
Tactic: refine (iff_adjoin_eq_top _ A _).2 ⟨fun s hs hs' ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs : s ∈ S ∪ {n}
hs' : s ≠ 0
⊢ ∃ (r : B), IsPrimitiveRoot r s
have hs₁ : s ∈ S ∨ s = n
Tactic: rw [mem_union, mem_singleton_iff] at hs
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs : s ∈ S ∨ s = n
hs' : s ≠ 0
⊢ ∃ (r : B), IsPrimitiveRoot r s
have refine_1 : ∀ (hs : s ∈ S), ∃ (r : B), IsPrimitiveRoot r s
Tactic: obtain hs | rfl := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S : Set ℕ
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
h : ∃ s ∈ S, s ≠ 0 ∧ n ∣ s
H : IsCyclotomicExtension S A B
s : ℕ
hs : s ∈ S ∨ s = n
hs' : s ≠ 0
refine_1 : ∀ (hs : s ∈ S), ∃ (r : B), IsPrimitiveRoot r s
⊢ ∃ (r : B), IsPrimitiveRoot r s
have refine_1₁ : ∀ [NeZero s] (h : ∃ s_1 ∈ S, s_1 ≠ 0 ∧ s ∣ s_1), ∃ (r : B), IsPrimitiveRoot r s
Tactic: obtain hs | rfl := hs
Cleared hypotheses: n, inst, h, hs
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
h : ∃ s_1 ∈ S, s_1 ≠ 0 ∧ s ∣ s_1
⊢ ∃ (r : B), IsPrimitiveRoot r s
have refine_1 : ∀ (x : ℕ) (hm : s * x ∈ S) (hm' : s * x ≠ 0), ∃ (r : B), IsPrimitiveRoot r s
Tactic: obtain ⟨m, hm, hm', ⟨x, rfl⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
⊢ ∃ (r : B), IsPrimitiveRoot r s
have refine_1 : ∀ (ζ : B) (hζ : IsPrimitiveRoot ζ (s * x)), ∃ (r : B), IsPrimitiveRoot r s
Tactic: obtain ⟨ζ, hζ⟩ := H.exists_isPrimitiveRoot hm hm'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
⊢ ∃ (r : B), IsPrimitiveRoot r s
have refine_1 : IsPrimitiveRoot (ζ ^ x) s
Tactic: refine ⟨ζ ^ x, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
⊢ IsPrimitiveRoot (ζ ^ x) s
have h_xnz : x ≠ 0
Tactic: have h_xnz : x ≠ 0 := Nat.ne_zero_of_mul_ne_zero_right hm'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
h_xnz : x ≠ 0
⊢ IsPrimitiveRoot (ζ ^ x) s
have this : IsPrimitiveRoot (ζ ^ x) (s * x / x)
Tactic: have := hζ.pow_of_dvd h_xnz (dvd_mul_left x s)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
H : IsCyclotomicExtension S A B
s : ℕ
hs' : s ≠ 0
inst_3 : NeZero s
x : ℕ
hm : s * x ∈ S
hm' : s * x ≠ 0
ζ : B
hζ : IsPrimitiveRoot ζ (s * x)
h_xnz : x ≠ 0
this : IsPrimitiveRoot (ζ ^ x) (s * x / x)
⊢ IsPrimitiveRoot (ζ ^ x) s
have refine_1 : ∀ (this : IsPrimitiveRoot (ζ ^ x) s), IsPrimitiveRoot (ζ ^ x) s
Tactic: rwa [mul_div_cancel_right₀ _ h_xnz] at this
Cleared hypotheses: this