awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y : AlgebraicClosure K
hy :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
⊢ Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K)
have right : ∀ (x : AlgebraicClosure K)
  (hx : Membership.mem (γ := Set (AlgebraicClosure K)) {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} x),
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
Tactic: induction hy using IntermediateField.adjoin_induction with
  | mem x hx =>
    obtain ⟨n, hn, h1, h2⟩ := hx
    apply IntermediateField.subset_adjoin
    use n, hn, h1
    rw [← map_pow, ← map_one f, h2]
  | algebraMap x =>
    convert! IntermediateField.algebraMap_mem _ x
    exact AlgHom.commutes _ x
  | add x y hx hy ihx ihy =>
    rw [map_add]
    exact add_mem ihx ihy
  | mul x y hx hy ihx ihy =>
    rw [map_mul]
    exact mul_mem ihx ihy
  | inv x hx ihx =>
    rw [map_inv₀]
    exact inv_mem ihx
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y : AlgebraicClosure K
hy :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
right :
  ∀ (x : AlgebraicClosure K)
    (hx : Membership.mem (γ := Set (AlgebraicClosure K)) {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} x),
    Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
      (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
⊢ Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K)
have right₁ : ∀ (x : K),
  Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K)
        ((algebraMap K (AlgebraicClosure K) : (a : K) → AlgebraicClosure K) x) :
      AlgebraicClosure K)
Tactic: induction hy using IntermediateField.adjoin_induction with
  | mem x hx =>
    obtain ⟨n, hn, h1, h2⟩ := hx
    apply IntermediateField.subset_adjoin
    use n, hn, h1
    rw [← map_pow, ← map_one f, h2]
  | algebraMap x =>
    convert! IntermediateField.algebraMap_mem _ x
    exact AlgHom.commutes _ x
  | add x y hx hy ihx ihy =>
    rw [map_add]
    exact add_mem ihx ihy
  | mul x y hx hy ihx ihy =>
    rw [map_mul]
    exact mul_mem ihx ihy
  | inv x hx ihx =>
    rw [map_inv₀]
    exact inv_mem ihx
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
⊢ Eq (α := Subalgebra K L) (adjoin K ((HPow.hPow (α := K[X]) X n - 1).rootSet L)) ⊤
have rw : Eq (α := Subalgebra K L) (adjoin K ((HPow.hPow (α := K[X]) X n - 1).rootSet L))
  (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
Tactic: rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
⊢ Eq (α := Subalgebra K L) (adjoin K ((HPow.hPow (α := K[X]) X n - 1).rootSet L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
have e_s : (HPow.hPow (α := K[X]) X n - 1).rootSet L =
  {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
⊢ (HPow.hPow (α := K[X]) X n - 1).rootSet L =
    {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}
have e_s : ∀ (x : L),
  x ∈ (HPow.hPow (α := K[X]) X n - 1).rootSet L ↔
    Membership.mem (γ := Set L) {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1} x
Tactic: refine Set.ext fun x => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
x : L
⊢ x ∈ (HPow.hPow (α := K[X]) X n - 1).rootSet L ↔
    Membership.mem (γ := Set L) {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1} x
have e_s : x ∈ (HPow.hPow (α := K[X]) X n - 1).rootSet L ↔ x ^ n = 1
Tactic: simp only [mem_singleton_iff, ne_eq, exists_eq_left, NeZero.ne, not_false_eq_true, true_and,
        mem_setOf_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
x : L
⊢ x ∈ (HPow.hPow (α := K[X]) X n - 1).rootSet L ↔ x ^ n = 1
have e_s : x ^ n = 1 → HPow.hPow (α := L[X]) X n - 1 ≠ 0
Tactic: simp only [mem_rootSet', map_sub, map_pow, aeval_one, aeval_X, sub_eq_zero, map_X,
        and_iff_right_iff_imp, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
⊢ Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L)) ⊤
have rw : Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L))
  (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
Tactic: rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
inst_4 : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
⊢ Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
have obtain : ∀ (ζ : L) (hζ : IsPrimitiveRoot ζ n),
  Eq (α := Subalgebra K L) (adjoin K (rootSet (cyclotomic n K) L))
    (adjoin K {b : L | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
Tactic: obtain ⟨ζ : L, hζ⟩ :=
        IsCyclotomicExtension.exists_isPrimitiveRoot K L (mem_singleton n) (NeZero.ne _)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
have this : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
Tactic: have : NeZero (n : CyclotomicField n K) :=
    NeZero.nat_of_injective (algebraMap K _).injective
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
have this₁ : degree (cyclotomic n K) ≠ 0
Tactic: have := (degree_cyclotomic_pos n K (NeZero.pos n)).ne'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
have obtain : ∀ (ζ : SplittingField (cyclotomic n K))
  (hζ : eval ζ (map (algebraMap K (SplittingField (cyclotomic n K))) (cyclotomic n K)) = 0),
  IsCyclotomicExtension {n} K (CyclotomicField n K)
Tactic: obtain ⟨ζ, hζ⟩ :=
    Splits.exists_eval_eq_zero (SplittingField.splits (cyclotomic n K)) (by rwa [degree_map])
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : eval ζ (map (algebraMap K (SplittingField (cyclotomic n K))) (cyclotomic n K)) = 0
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
have hζ₁ : IsPrimitiveRoot ζ n
Tactic: rw [eval_map, ← eval_map, ← IsRoot.def, map_cyclotomic, isRoot_cyclotomic_iff] at hζ
Cleared hypotheses: hζ
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
have refine_1 : ∀ {n_1 : ℕ} (ha : Membership.mem (γ := Set ℕ) {n} n_1) (ha' : n_1 ≠ 0),
  ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n_1
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
refine_1 :
  ∀ {n_1 : ℕ} (ha : Membership.mem (γ := Set ℕ) {n} n_1) (ha' : n_1 ≠ 0),
    ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n_1
⊢ IsCyclotomicExtension {n} K (CyclotomicField n K)
have refine_2 : ∀ (x : CyclotomicField n K),
  Membership.mem (γ := Subalgebra K (CyclotomicField n K))
    (adjoin K {b : CyclotomicField n K | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}) x
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
⊢ ∀ {n_1 : ℕ} (ha : Membership.mem (γ := Set ℕ) {n} n_1) (ha' : n_1 ≠ 0),
    ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n_1
have refine_1 : ∀ (ha' : n ≠ 0), ∃ (r : CyclotomicField n K), IsPrimitiveRoot r n
Tactic: simp only [mem_singleton_iff, forall_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : NeZero.{w} (R := K) (↑n : K)
this_1 : NeZero.{w} (R := CyclotomicField n K) (↑n : CyclotomicField n K)
this_2 : DecidableEq (CyclotomicField n K) := Classical.decEq (CyclotomicField n K)
this : degree (cyclotomic n K) ≠ 0
ζ : SplittingField (cyclotomic n K)
hζ : IsPrimitiveRoot ζ n
⊢ ∀ (x : CyclotomicField n K),
    Membership.mem (γ := Subalgebra K (CyclotomicField n K))
      (adjoin K {b : CyclotomicField n K | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1}) x
have refine_2 : Eq (α := Subalgebra K (CyclotomicField n K)) (adjoin K (rootSet (cyclotomic n K) (SplittingField (cyclotomic n K))))
  (adjoin K {b : CyclotomicField n K | ∃ (n_1 : ℕ), Membership.mem (γ := Set ℕ) {n} n_1 ∧ n_1 ≠ 0 ∧ b ^ n_1 = 1})
Tactic: rw [← Algebra.eq_top_iff, ← SplittingField.adjoin_rootSet, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
inst : NeZero n
S 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
x : CyclotomicField 0 K
⊢ finrank K (CyclotomicField 0 K) = 1
have this : IsSplittingField K K (cyclotomic 0 K)
Tactic: have : Polynomial.IsSplittingField K K (Polynomial.cyclotomic 0 K) :=
        Polynomial.isSplittingField_C 1
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
inst : NeZero n
S 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
x : CyclotomicField 0 K
⊢ Membership.mem (γ := Subalgebra K (CyclotomicField 0 K))
    (adjoin K {b : CyclotomicField 0 K | ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {0} n ∧ n ≠ 0 ∧ b ^ n = 1}) x
have finrank : finrank K (CyclotomicField 0 K) = 1
Tactic: have finrank : Module.finrank K (CyclotomicField 0 K) = 1 := by
      have : Polynomial.IsSplittingField K K (Polynomial.cyclotomic 0 K) :=
        Polynomial.isSplittingField_C 1
      let e : K ≃ₗ[K] (CyclotomicField 0 K) :=
        (Polynomial.IsSplittingField.algEquiv K (Polynomial.cyclotomic 0 K)).toLinearEquiv
      simp [← LinearEquiv.finrank_eq e, finrank_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : Algebra A K
inst_8 : IsDomain A
inst_9 : IsFractionRing A K
⊢ IsTorsionFree.{u, w} A (CyclotomicField n K)
have rw : Function.Injective.{u + 1, w + 1} (α := A) (β := CyclotomicField n K)
  (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K (CyclotomicField n K)) (algebraMap A K)) :
    (a : A) → CyclotomicField n K)
Tactic: rw [isTorsionFree_iff_faithfulSMul, faithfulSMul_iff_algebraMap_injective,
    IsScalarTower.algebraMap_eq A K (CyclotomicField n K)]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x_1 : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x
⊢ IsUnit (M := CyclotomicField n K)
    ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
        (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
              Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
          CyclotomicRing n A K) :
      CyclotomicField n K)
have rw : Ne (α := CyclotomicField n K)
  ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
            Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
        CyclotomicRing n A K) :
    CyclotomicField n K)
  (0 : CyclotomicField n K)
Tactic: rw [isUnit_iff_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x_1 : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x
⊢ Ne (α := CyclotomicField n K)
    ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
        (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
              Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
          CyclotomicRing n A K) :
      CyclotomicField n K)
    (0 : CyclotomicField n K)
have hg : Function.Injective.{w + 1, w + 1} (α := CyclotomicRing n A K) (β := CyclotomicField n K)
  (⇑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) : (a : CyclotomicRing n A K) → CyclotomicField n K)
Tactic: apply map_ne_zero_of_mem_nonZeroDivisors
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x_1 : ↥(nonZeroDivisors (CyclotomicRing n A K))
x : CyclotomicRing n A K
hx : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x
hg :
  Function.Injective.{w + 1, w + 1} (α := CyclotomicRing n A K) (β := CyclotomicField n K)
    (⇑(algebraMap (CyclotomicRing n A K) (CyclotomicField n K)) : (a : CyclotomicRing n A K) → CyclotomicField n K)
⊢ Ne (α := CyclotomicField n K)
    ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
        (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
              Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
          CyclotomicRing n A K) :
      CyclotomicField n K)
    (0 : CyclotomicField n K)
have h : Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K))
  (↑(Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
        Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x) x hx) :
    CyclotomicRing n A K)
Tactic: apply map_ne_zero_of_mem_nonZeroDivisors
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
inst : NeZero n
S 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 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
⊢ ∃ (x_1 : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) x
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            (↑x_1.2 : CyclotomicRing n A K) :
          CyclotomicField n K) =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x_1.1
have this : NeZero.{w} (R := K) (↑n : K)
Tactic: have : NeZero (n : K) := NeZero.nat_of_injective (IsFractionRing.injective A K)
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
n : ℕ
inst : NeZero n
S 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 : Algebra A K
inst_8 : IsFractionRing A K
inst_9 : IsDomain A
inst_10 : NeZero.{u} (R := A) (↑n : A)
x : CyclotomicField n K
this : NeZero.{w} (R := K) (↑n : K)
⊢ ∃ (x_1 : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) x
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            (↑x_1.2 : CyclotomicRing n A K) :
          CyclotomicField n K) =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x_1.1
have refine_1 : ∀ (y : CyclotomicField n K)
  (hy : Membership.mem (γ := Set (CyclotomicField n K)) {b : CyclotomicField n K | b ^ n = 1} y),
  ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) y
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            (↑x.2 : CyclotomicRing n A K) :
          CyclotomicField n K) =
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x.1
Tactic: refine
      Algebra.adjoin_induction
        (hx := ((IsCyclotomicExtension.iff_singleton n K (CyclotomicField n K)).1
            (CyclotomicField.isCyclotomicExtension n K)).2 x)
        (fun y hy => ?_) (fun k => ?_) ?_ ?_