awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ ∃ (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_2 : ∀ (k : K),
  ∃ (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
      Algebra.adjoin_induction
        (hx := ((IsCyclotomicExtension.iff_singleton n K (CyclotomicField n K)).1
            (CyclotomicField.isCyclotomicExtension n K)).2 x)
        (fun y hy => ?_) (fun 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)
y : CyclotomicField n K
hy : Membership.mem (γ := Set (CyclotomicField n K)) {b : CyclotomicField n K | b ^ n = 1} y
⊢ y *
      (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
        (↑(Subtype.mk (p := fun (x : CyclotomicField n K) ↦
                  Membership.mem (γ := Subalgebra A (CyclotomicField n K))
                    (adjoin A {b : CyclotomicField n K | b ^ n = 1}) x)
                  y ⋯,
                1).2 :
          CyclotomicRing n A K) =
    (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
      (Subtype.mk (p := fun (x : CyclotomicField n K) ↦
            Membership.mem (γ := Subalgebra A (CyclotomicField n K)) (adjoin A {b : CyclotomicField n K | b ^ n = 1}) x)
            y ⋯,
          1).1
have simp : y =
  (algebraMap (CyclotomicRing n A K) (CyclotomicField n K) : (a : CyclotomicRing n A K) → CyclotomicField n K)
    (Subtype.mk (p := fun (x : CyclotomicField n K) ↦
      Membership.mem (γ := Subalgebra A (CyclotomicField n K)) (adjoin A {b : CyclotomicField n K | b ^ n = 1}) x) y sorry)
Tactic: simp
-- 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
this : NeZero.{w} (R := K) (↑n : K)
k : K
⊢ ∃ (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
have this₁ : IsLocalization.{u, w} (R := A) (nonZeroDivisors A) K
Tactic: have : IsLocalization (nonZeroDivisors A) K := inferInstance
-- 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
this_1 : NeZero.{w} (R := K) (↑n : K)
k : K
this : IsLocalization.{u, w} (R := A) (nonZeroDivisors A) K
⊢ ∃ (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
have 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
Tactic: replace := this.surj
Cleared hypotheses: this
-- 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_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
⊢ ∃ (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
have 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
Tactic: obtain ⟨⟨z, w⟩, hw⟩ := this 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_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
have 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)) sorry).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)) sorry).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⟩, ?_⟩
-- 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_1 : NeZero.{w} (R := K) (↑n : K)
k : K
this_2 :
  ∀ (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
this : IsScalarTower A K (CyclotomicField n 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)
          (↑((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
have 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 A (CyclotomicField n K) : (a : A) → CyclotomicField n K) (↑w : A) : 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)) sorry).1
Tactic: rw [← IsScalarTower.algebraMap_apply, ← IsScalarTower.algebraMap_apply,
        @IsScalarTower.algebraMap_apply A K _ _ _ _ _ (_root_.CyclotomicField.algebra n K) _ _ w,
        ← map_mul, hw, ← IsScalarTower.algebraMap_apply]
-- 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)
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
have 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)) sorry).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)) sorry).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⟩⟩, ?_⟩
-- 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)
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
have 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)) sorry).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)) sorry).1
Tactic: refine ⟨⟨a.1 * b.1, a.2 * b.2, mul_mem_nonZeroDivisors.2 ⟨a.2.2, b.2.2⟩⟩, ?_⟩
-- 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)
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) (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
have refine_4 : 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)) sorry).1
Tactic: rw [map_mul, mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), mul_assoc, ←
        mul_assoc z, hb, ← mul_comm ((algebraMap (CyclotomicRing n A K) _) ↑a.2), ← mul_assoc, ha]
-- 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 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)
⊢ (↑1 : CyclotomicRing n A K) * x = (↑1 : CyclotomicRing n A K) * y
have rw : (↑1 : CyclotomicRing n A K) * y = (↑1 : CyclotomicRing n A K) * y
Tactic: rw [adjoin_algebra_injective n A K h]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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 = ↥A[μ]
have rw : CyclotomicRing n A K =
  ↥(adjoin A {b : CyclotomicField n K | ∃ (a : ℕ), Membership.mem (γ := Set ℕ) {n} a ∧ a ≠ 0 ∧ b ^ a = 1})
Tactic: rw [← IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic h,
    IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots h]