awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
⊢ IsCyclotomicExtension S K K
have refine : ∀ {a : ℕ} (ha : a ∈ S) (ha' : a ≠ 0), ∃ (r : K), IsPrimitiveRoot r a
Tactic: refine ⟨fun {a} ha ha' ↦ ?_, Algebra.eq_top_iff.mp <| Subsingleton.elim _ _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
⊢ ∃ (r : K), IsPrimitiveRoot r a
have this : NeZero.{w} (R := K) (↑a : K)
Tactic: have := h a ha ha'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero.{w} (R := K) (↑a : K)
⊢ ∃ (r : K), IsPrimitiveRoot r a
have obtain : ∀ (r : K) (hr : Eq (α := K) ((aeval r : (a : K[X]) → K) (cyclotomic a K) : K) (0 : K)), ∃ (r : K), IsPrimitiveRoot r a
Tactic: obtain ⟨r, hr⟩ := IsSepClosed.exists_aeval_eq_zero K _
    (degree_cyclotomic_pos a K (Nat.pos_of_ne_zero ha')).ne' (separable_cyclotomic a K)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero.{w} (R := K) (↑a : K)
r : K
hr : Eq (α := K) ((aeval r : (a : K[X]) → K) (cyclotomic a K) : K) (0 : K)
⊢ IsPrimitiveRoot r a
have rwa : ∀ (hr : eval r (cyclotomic a K) = 0), IsPrimitiveRoot r a
Tactic: rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero.{w} (R := K) (↑a : K)
r : K
hr : Eq (α := K) ((aeval r : (a : K[X]) → K) (cyclotomic a K) : K) (0 : K)
rwa : ∀ (hr : eval r (cyclotomic a K) = 0), IsPrimitiveRoot r a
⊢ IsPrimitiveRoot r a
have rwa₁ : ∀ (hr : IsRoot (cyclotomic a K) r), IsPrimitiveRoot r a
Tactic: rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
a : ℕ
ha : a ∈ S
ha' : a ≠ 0
this : NeZero.{w} (R := K) (↑a : K)
r : K
hr : Eq (α := K) ((aeval r : (a : K[X]) → K) (cyclotomic a K) : K) (0 : K)
rwa : ∀ (hr : eval r (cyclotomic a K) = 0), IsPrimitiveRoot r a
rwa₁ : ∀ (hr : IsRoot (cyclotomic a K) r), IsPrimitiveRoot r a
⊢ IsPrimitiveRoot r a
have rwa₂ : ∀ (hr : IsPrimitiveRoot r a), IsPrimitiveRoot r a
Tactic: rwa [coe_aeval_eq_eval, ← IsRoot.def, isRoot_cyclotomic_iff] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S_1 T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : IsSepClosed K
inst_8 : CharZero K
S : Set ℕ
⊢ IsCyclotomicExtension S K K
have rw : IsCyclotomicExtension (S \ {0}) K K
Tactic: rw [IsCyclotomicExtension.eq_self_sdiff_zero]
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
⊢ ζ ∈ C
have obtain : ∀ (η : ↥C) (hη : IsPrimitiveRoot η m), ζ ∈ C
Tactic: obtain ⟨η, hη⟩ := h.1 h₁ h₂
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
η : ↥C
hη : IsPrimitiveRoot η m
⊢ ζ ∈ C
have hη₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
Tactic: replace hη := hη.map_of_injective (FaithfulSMul.algebraMap_injective C B)
Cleared hypotheses: hη
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
η : ↥C
hη : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
⊢ ζ ∈ C
have this : NeZero m
Tactic: have : NeZero m := ⟨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
inst_3 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
ζ : B
h₁ : m ∈ S
h₂ : m ≠ 0
hζ : ζ ^ m = 1
η : ↥C
hη : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
this : NeZero m
⊢ ζ ∈ C
have obtain : ∀ k < m,
  ∀ (hζ : HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ^ m = 1),
    HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ∈ C
Tactic: obtain ⟨k, _, rfl⟩ := hη.eq_pow_of_pow_eq_one 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
inst_3 : IsDomain B
C : Subalgebra A B
h : IsCyclotomicExtension.{u, v} S A ↥C
m : ℕ
h₁ : m ∈ S
h₂ : m ≠ 0
η : ↥C
hη : IsPrimitiveRoot (M := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) m
this : NeZero m
k : ℕ
left : k < m
hζ : HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ^ m = 1
⊢ HPow.hPow (α := B) ((algebraMap (↥C) B : (a : ↥C) → B) η : B) k ∈ C
have rw : Membership.mem (α := B) C ((algebraMap (↥C) B : (a : ↥C) → B) (η ^ k) : B)
Tactic: rw [← map_pow]
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
⊢ IsCyclotomicExtension.{u, v} S A ↥C ↔ C = adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
have refine : ∀ (h : IsCyclotomicExtension.{u, v} S A ↥C), C = adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ isCyclotomicExtension_adjoin_of_exists_isPrimitiveRoot S A B hS⟩
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
⊢ C = adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
have this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
Tactic: have := congr_arg (Subalgebra.map C.val) ((IsCyclotomicExtension.iff_adjoin_eq_top _ _ _).mp h).2
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
⊢ C = adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
have rw : Eq (α := Subalgebra A B) (adjoin A (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
  (adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
Tactic: rw [← Subalgebra.range_val C, ← Algebra.map_top, ← this, AlgHom.map_adjoin]
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
⊢ Eq (α := Subalgebra A B) (adjoin A (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
have e_s : Eq (α := Set B) (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
  {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Tactic: congr
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
⊢ Eq (α := Set B) (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
have e_s : ∀ (x : B),
  Membership.mem (γ := Set B) (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x ↔
    Membership.mem (γ := Set B) {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} x
Tactic: ext
-- 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
inst_3 : IsDomain B
C : Subalgebra A B
hS : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
h : IsCyclotomicExtension.{u, v} S A ↥C
this : Subalgebra.map C.val (adjoin A {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) = Subalgebra.map C.val ⊤
x : B
⊢ Membership.mem (γ := Set B) (image (α := ↥C) (⇑C.val : (a : ↥C) → B) {b : ↥C | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x ↔
    Membership.mem (γ := Set B) {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} x
have e_s : ∀ x_1 ∈ S, ¬x_1 = 0 → x ^ x_1 = 1 → x ∈ C
Tactic: simp only [Subalgebra.coe_val, ne_eq, ← Subalgebra.coe_eq_one, SubmonoidClass.coe_pow,
    Set.mem_image, Set.mem_setOf_eq, Subtype.exists, exists_and_left, exists_prop,
    exists_eq_right_right, and_iff_left_iff_imp, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension.{u, v} {n} A ↥C ↔ C = A[ζ]
have rw : C = adjoin A {x : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1} ↔ C = A[ζ]
Tactic: rw [isCyclotomicExtension_iff_eq_adjoin]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
rw : C = adjoin A {x : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1} ↔ C = A[ζ]
⊢ IsCyclotomicExtension.{u, v} {n} A ↥C ↔ C = A[ζ]
have hS : ∀ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 → n_1 ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n_1
Tactic: rw [isCyclotomicExtension_iff_eq_adjoin]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ C = adjoin A {x : B | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ x ^ n_1 = 1} ↔ C = A[ζ]
have simp : C = adjoin A {x : B | n ≠ 0 ∧ x ^ n = 1} ↔ C = A[ζ]
Tactic: simp only [Set.mem_singleton_iff, exists_eq_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
this : Eq (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
⊢ C = adjoin A {x : B | n ≠ 0 ∧ x ^ n = 1} ↔ C = A[ζ]
have rw : C = A[ζ] ↔ C = A[ζ]
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ C = adjoin A {x : B | n ≠ 0 ∧ x ^ n = 1} ↔ C = A[ζ]
have suffices : Eq (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
Tactic: suffices adjoin A {b | n ≠ 0 ∧ b ^ n = 1} = adjoin A {ζ} by rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ Eq (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
have a : LE.le (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
a : LE.le (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
⊢ Eq (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
have a₁ : LE.le (α := Subalgebra A B) A[ζ] (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
⊢ LE.le (α := Subalgebra A B) (adjoin A {b : B | n ≠ 0 ∧ b ^ n = 1}) A[ζ]
have a : ∀ (x : B), Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x → n ≠ 0 → ∀ (hx : x ^ n = 1), x ∈ (↑A[ζ] : Set B)
Tactic: refine adjoin_le fun x ⟨_, hx⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : IsDomain B
C : Subalgebra A B
ζ : B
hζ : IsPrimitiveRoot ζ n
x : B
h : Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} x
left : n ≠ 0
hx : x ^ n = 1
⊢ x ∈ (↑A[ζ] : Set B)
have a : ∀ k < n,
  Membership.mem (γ := Set B) {b : B | n ≠ 0 ∧ b ^ n = 1} (ζ ^ k) → ∀ (hx : (ζ ^ k) ^ n = 1), ζ ^ k ∈ (↑A[ζ] : Set B)
Tactic: obtain ⟨k, _, rfl⟩ := hζ.eq_pow_of_pow_eq_one hx
Cleared hypotheses: x, h, hx
-- 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
inst_3 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
n : ℕ
hn₁ : n ∈ S
hn₂ : n ≠ 0
⊢ ∃ (x : B), IsPrimitiveRoot x n
have obtain : ∀ (ζ : ↥C₁) (hζ : IsPrimitiveRoot ζ n), ∃ (x : B), IsPrimitiveRoot x n
Tactic: obtain ⟨ζ, hζ⟩ := h₁.1 hn₁ hn₂
-- 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
inst_3 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
⊢ C₁ = C₂
have hC : ∀ (n : ℕ) (hn₁ : n ∈ S) (hn₂ : n ≠ 0), ∃ (x : B), IsPrimitiveRoot x n
Tactic: have hC (n) (hn₁ : n ∈ S) (hn₂ : n ≠ 0) : ∃ x : B, IsPrimitiveRoot x n := by
    obtain ⟨ζ, hζ⟩ := h₁.1 hn₁ hn₂
    exact ⟨ζ, IsPrimitiveRoot.coe_submonoidClass_iff.mpr 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
inst_3 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
hC : ∀ (n : ℕ) (hn₁ : n ∈ S) (hn₂ : n ≠ 0), ∃ (x : B), IsPrimitiveRoot x n
⊢ C₁ = C₂
have rw : adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = C₂
Tactic: rw [(isCyclotomicExtension_iff_eq_adjoin S C₁ hC).mp h₁,
    (isCyclotomicExtension_iff_eq_adjoin S C₂ hC).mp 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
inst_3 : IsDomain B
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} S A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} S A ↥C₂
hC : ∀ (n : ℕ) (hn₁ : n ∈ S) (hn₂ : n ≠ 0), ∃ (x : B), IsPrimitiveRoot x n
rw : adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} = C₂
⊢ C₁ = C₂
have rw₁ : Eq.{v + 1} (α := Subalgebra A B) (adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
  (adjoin A {x : B | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
Tactic: rw [(isCyclotomicExtension_iff_eq_adjoin S C₁ hC).mp h₁,
    (isCyclotomicExtension_iff_eq_adjoin S C₂ hC).mp h₂]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
⊢ NeZero n₁
have out : n₁ ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
⊢ C₁ ≤ C₂
have this : NeZero n₁
Tactic: have : NeZero n₁ := by
    constructor
    rintro rfl
    exact NeZero.ne n₂ <| eq_zero_of_zero_dvd h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
this : NeZero n₁
⊢ C₁ ≤ C₂
have obtain : ∀ (ζ₂ : ↥C₂) (hζ₂ : IsPrimitiveRoot ζ₂ n₂), C₁ ≤ C₂
Tactic: obtain ⟨ζ₂, hζ₂⟩ := h₂.1 rfl (NeZero.ne n₂)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
⊢ C₁ ≤ C₂
have hζ₃ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
Tactic: replace hζ₂ := hζ₂.map_of_injective (FaithfulSMul.algebraMap_injective C₂ B)
Cleared hypotheses: hζ₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
⊢ C₁ ≤ C₂
have obtain : ∀ (d : ℕ) (hd : n₂ = n₁ * d), C₁ ≤ C₂
Tactic: obtain ⟨d, hd⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
d : ℕ
hd : n₂ = n₁ * d
⊢ C₁ ≤ C₂
have hζ₁ : IsPrimitiveRoot (HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) d) n₁
Tactic: have hζ₁ := IsPrimitiveRoot.pow n₂.pos_of_neZero hζ₂ (by rwa [mul_comm])
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
have obtain : ∀ (ζ₁ : ↥C₁) (hζ₁ : IsPrimitiveRoot ζ₁ n₁), IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
Tactic: obtain ⟨ζ₁, hζ₁⟩ := h₁.1 rfl (NeZero.ne n₁)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
have obtain : ∀ (ζ₂ : ↥C₂) (hζ₂ : IsPrimitiveRoot ζ₂ n₂), IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
Tactic: obtain ⟨ζ₂, hζ₂⟩ := h₂.1 rfl (NeZero.ne n₂)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
have hζ₃ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
Tactic: replace hζ₁ := hζ₁.map_of_injective (FaithfulSMul.algebraMap_injective C₁ B)
Cleared hypotheses: hζ₁
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
have hζ₃ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
Tactic: replace hζ₂ := hζ₂.map_of_injective (FaithfulSMul.algebraMap_injective C₂ B)
Cleared hypotheses: hζ₂
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
have hζ : IsPrimitiveRoot
  (HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
    HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂))
  (n₁.lcm n₂)
Tactic: have hζ := hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)