awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_1 : NeZero.{w} (R := K) (↑n : K)
k : K
this : IsLocalization.{u, w} (R := A) (nonZeroDivisors A) K
⊢ ∀ (z : K),
    ∃ (x : A × ↥(nonZeroDivisors A : Submonoid A)),
      HMul.hMul (β := K) z ((algebraMap A K : (a : A) → K) (↑x.2 : A) : K) = (algebraMap A K : (a : A) → K) x.1

Tactic:
replace := this.surj
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_1 : NeZero.{w} (R := K) (↑n : K)
k : K
this :
  ∀ (z : K),
    ∃ (x : A × ↥(nonZeroDivisors A : Submonoid A)),
      HMul.hMul (β := K) z ((algebraMap A K : (a : A) → K) (↑x.2 : A) : K) = (algebraMap A K : (a : A) → K) x.1
refine_2 :
  ∀ (z : A) (w : ↥(nonZeroDivisors A : Submonoid A))
    (hw :
      HMul.hMul (β := K) k ((algebraMap A K : (a : A) → K) (↑(z, w).2 : A) : K) =
        (algebraMap A K : (a : A) → K) (z, w).1),
    ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
      HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
          ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
          ((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
⊢ ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
        ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
        ((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:
obtain ⟨⟨z, w⟩, hw⟩ := this k
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_1 : NeZero.{w} (R := K) (↑n : K)
k : K
this :
  ∀ (z : K),
    ∃ (x : A × ↥(nonZeroDivisors A : Submonoid A)),
      HMul.hMul (β := K) z ((algebraMap A K : (a : A) → K) (↑x.2 : A) : K) = (algebraMap A K : (a : A) → K) x.1
z : A
w : ↥(nonZeroDivisors A : Submonoid A)
hw : HMul.hMul (β := K) k ((algebraMap A K : (a : A) → K) (↑(z, w).2 : A) : K) = (algebraMap A K : (a : A) → K) (z, w).1
⊢ ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
        ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
        ((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:
⟨⟨algebraMap A (CyclotomicRing n A K) z, algebraMap A (CyclotomicRing n A K) w,
        map_mem_nonZeroDivisors _ (algebraBase_injective n A K) w.2⟩, ?_⟩

Premises used: Algebra.algebraMap, Prod.mk, map_mem_nonZeroDivisors, Subtype.mk, CyclotomicRing.algebraBase_injective, Exists.intro, Subtype.val, CyclotomicRing, DFunLike.coe, Subtype.property
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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_1 : NeZero.{w} (R := K) (↑n : K)
k : K
this :
  ∀ (z : K),
    ∃ (x : A × ↥(nonZeroDivisors A : Submonoid A)),
      HMul.hMul (β := K) z ((algebraMap A K : (a : A) → K) (↑x.2 : A) : K) = (algebraMap A K : (a : A) → K) x.1
z : A
w : ↥(nonZeroDivisors A : Submonoid A)
hw : HMul.hMul (β := K) k ((algebraMap A K : (a : A) → K) (↑(z, w).2 : A) : K) = (algebraMap A K : (a : A) → K) (z, w).1
refine_2 :
  HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
      ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) z,
                  Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
                    Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
                    ((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) (↑w : A)) ⋯).2 :
            CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      ((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) z,
          Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
            Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
            ((algebraMap A (CyclotomicRing n A K) : (a : A) → CyclotomicRing n A K) (↑w : A)) ⋯).1
⊢ ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
        ((algebraMap K (CyclotomicField n K) : (a : K) → CyclotomicField n K) k : CyclotomicField n K)
        ((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 ⟨⟨algebraMap A (CyclotomicRing n A K) z, algebraMap A (CyclotomicRing n A K) w,
        map_mem_nonZeroDivisors _ (algebraBase_injective n A K) w.2⟩, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  HMul.hMul (β := CyclotomicField n K) y
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑a.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  HMul.hMul (β := CyclotomicField n K) z
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑b.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) b.1
⊢ ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) (y + z)
        ((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:
⟨⟨a.1 * b.2 + b.1 * a.2, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Prod.mk, Prod.fst, Subtype.mk, HAdd.hAdd, And.intro, Exists.intro, Subtype.val, Prod.snd, mul_mem_nonZeroDivisors, Subtype.property
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  HMul.hMul (β := CyclotomicField n K) y
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑a.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  HMul.hMul (β := CyclotomicField n K) z
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑b.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) b.1
refine_3 :
  HMul.hMul (β := CyclotomicField n K) (y + z)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑(a.1 * (↑b.2 : CyclotomicRing n A K) + b.1 * (↑a.2 : 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)
                    ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) ⋯).2 :
            CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (a.1 * (↑b.2 : CyclotomicRing n A K) + b.1 * (↑a.2 : 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)
            ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) ⋯).1
⊢ ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) (y + z)
        ((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 ⟨⟨a.1 * b.2 + b.1 * a.2, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  HMul.hMul (β := CyclotomicField n K) y
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑a.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  HMul.hMul (β := CyclotomicField n K) z
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑b.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) b.1
⊢ HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            a.1 :
          CyclotomicField n K)
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            (↑b.2 : CyclotomicRing n A K) :
          CyclotomicField n K) +
      HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            b.1 :
          CyclotomicField n K)
        ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
            (↑a.2 : CyclotomicRing n A K) :
          CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (a.1 * (↑b.2 : CyclotomicRing n A K) + b.1 * (↑a.2 : 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)
            ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) ⋯).1

Tactic:
simp only [map_add, map_mul]

Premises used: map_add, map_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  HMul.hMul (β := CyclotomicField n K) y
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑a.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  HMul.hMul (β := CyclotomicField n K) z
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑b.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) b.1
⊢ ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) (y * z)
        ((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:
⟨⟨a.1 * b.1, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩

Premises used: Iff.mpr, HMul.hMul, Prod.mk, Prod.fst, Subtype.mk, And.intro, Exists.intro, Subtype.val, Prod.snd, mul_mem_nonZeroDivisors, Subtype.property
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  HMul.hMul (β := CyclotomicField n K) y
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑a.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  HMul.hMul (β := CyclotomicField n K) z
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑b.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) b.1
refine_4 :
  HMul.hMul (β := CyclotomicField n K) (y * z)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑(a.1 * b.1,
                  Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
                    Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
                    ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) ⋯).2 :
            CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (a.1 * b.1,
          Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
            Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
            ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) ⋯).1
⊢ ∃ (x : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))),
    HMul.hMul (β := CyclotomicField n K) (y * z)
        ((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 ⟨⟨a.1 * b.1, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
y z : CyclotomicField n K
a : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
ha :
  HMul.hMul (β := CyclotomicField n K) y
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑a.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) a.1
b : CyclotomicRing n A K × ↥(nonZeroDivisors (CyclotomicRing n A K))
hb :
  HMul.hMul (β := CyclotomicField n K) z
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          (↑b.2 : CyclotomicRing n A K) :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) b.1
⊢ HMul.hMul (α := CyclotomicField n K) (β := CyclotomicField n K)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          a.1 :
        CyclotomicField n K)
      ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
          b.1 :
        CyclotomicField n K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (a.1 * b.1,
          Subtype.mk (p := fun (x : CyclotomicRing n A K) ↦
            Membership.mem (γ := Submonoid (CyclotomicRing n A K)) (nonZeroDivisors (CyclotomicRing n A K)) x)
            ((↑a.2 : CyclotomicRing n A K) * (↑b.2 : CyclotomicRing n A K)) ⋯).1

Tactic:
simp only [map_mul]

Premises used: map_mul
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 y : CyclotomicRing n A K
h :
  Eq (α := CyclotomicField n K)
    ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) x :
      CyclotomicField n K)
    ((algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K) y :
      CyclotomicField n K)
rw rw₁ : (↑1 : CyclotomicRing n A K) * y = (↑1 : CyclotomicRing n A K) * y
⊢ (↑1 : CyclotomicRing n A K) * x = (↑1 : CyclotomicRing n A K) * y

Tactic:
rw [adjoin_algebra_injective n A K h]

Premises used: CyclotomicRing.adjoin_algebra_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
K : Type w
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ n
rw :
  CyclotomicRing n A K =
    ↥(adjoin A {b : CyclotomicField n K | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1})
⊢ CyclotomicRing n A K = ↥A[μ]

Tactic:
rw [← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,
    IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h]

Premises used: IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
K : Type w
inst_1 : CommRing A
inst_2 : Field K
inst_3 : Algebra A K
μ : CyclotomicField n K
h : IsPrimitiveRoot μ n
⊢ CyclotomicRing n A K =
    ↥(adjoin A {b : CyclotomicField n K | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1})

Tactic:
simp [CyclotomicRing, NeZero.ne n]

Premises used: CyclotomicRing, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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

Tactic:
⟨fun {a} ha ha' ↦ ?_, Algebra.eq_top_iff.mp <| Subsingleton.elim _ _⟩

Premises used: IsCyclotomicExtension.mk, Iff.mp, Algebra.eq_top_iff, Subsingleton.elim
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
inst : Field K
inst_1 : IsSepClosed K
h : ∀ a ∈ S, a ≠ 0 → NeZero.{w} (R := K) (↑a : K)
refine : ∀ {a : ℕ} (ha : a ∈ S) (ha' : a ≠ 0), ∃ (r : K), IsPrimitiveRoot r a
⊢ IsCyclotomicExtension S K K

Tactic:
refine ⟨fun {a} ha ha' ↦ ?_, Algebra.eq_top_iff.mp <| Subsingleton.elim _ _⟩