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
M : Type u_1
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
⊢ Eq.{u_1 + 1} (α := IntermediateField K M)
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
    (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
have a : LE.le.{u_1} (α := IntermediateField K M)
  (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
  (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
Tactic: apply le_antisymm
-- 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
M : Type u_1
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
a :
  LE.le.{u_1} (α := IntermediateField K M)
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
    (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
⊢ Eq.{u_1 + 1} (α := IntermediateField K M)
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
    (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
have a₁ : LE.le.{u_1} (α := IntermediateField K M) (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
  (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
Tactic: apply le_antisymm
-- 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
M : Type u_1
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
⊢ LE.le.{u_1} (α := IntermediateField K M)
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
    (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
have a : image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} ⊆
  (↑(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) : Set M)
Tactic: rw [IntermediateField.adjoin_le_iff]
-- 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
M : Type u_1
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
⊢ LE.le.{u_1} (α := IntermediateField K M) (IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    (IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
have a : {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} ⊆
  (↑(IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})) :
    Set M)
Tactic: rw [IntermediateField.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
M : Type u_1
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsSepClosed M
this : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
x : M
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
⊢ x ∈
    (↑(IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})) :
      Set M)
have this₁ : NeZero n
Tactic: have : NeZero n := ⟨h1⟩
-- 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
M : Type u_1
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsSepClosed M
this_1 : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
x : M
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
this : NeZero n
⊢ x ∈
    (↑(IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})) :
      Set M)
have a : ∀ (y : L) (hy : IsPrimitiveRoot y n),
  x ∈
    (↑(IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})) :
      Set M)
Tactic: obtain ⟨y, hy⟩ := exists_isPrimitiveRoot K L hn h1
-- 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
M : Type u_1
inst_4 : Field M
inst_5 : Algebra K M
inst_6 : IsSepClosed M
this_1 : Algebra.IsSeparable K L
i : L →ₐ[K] M := IsSepClosed.lift
htop : Eq.{z + 1} (α := IntermediateField K L) (IntermediateField.adjoin K {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ⊤
x : M
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
this : NeZero n
y : L
hy : IsPrimitiveRoot y n
⊢ x ∈
    (↑(IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})) :
      Set M)
have a : ∀ (m : ℕ) (h2 : HPow.hPow (α := M) ((i.toRingHom : (a : L) → M) y : M) m ^ n = 1),
  HPow.hPow (α := M) ((i.toRingHom : (a : L) → M) y : M) m ∈
    (↑(IntermediateField.adjoin K (image.{z, u_1} (α := L) (⇑i : (a : L) → M) {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})) :
      Set M)
Tactic: obtain ⟨m, -, rfl⟩ := (hy.map_of_injective i.injective).eq_pow_of_pow_eq_one h2
Cleared hypotheses: x, h2
-- 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
⊢ IsGalois K L
have rw : Algebra.IsSeparable K L ∧ Normal K L
Tactic: rw [isGalois_iff]
-- 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
⊢ Algebra.IsSeparable K L ∧ Normal K L
have right : Normal K L
Tactic: use isSeparable S K L
-- 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
⊢ Normal K L
have right : ∀ (i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})), Normal K L
Tactic: obtain ⟨i⟩ := nonempty_algEquiv_adjoin_of_isSepClosed S K L (AlgebraicClosure K)
-- 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})
⊢ Normal K L
have right : ∀ (σ : AlgebraicClosure K →ₐ[K] AlgebraicClosure K),
  IntermediateField.map σ (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) ≤
    IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
Tactic: rw [i.transfer_normal, IntermediateField.normal_iff_forall_map_le]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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
x : AlgebraicClosure K
hx : x ∈ IntermediateField.map f (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
⊢ Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
have hx₁ : ∃ (x_1 : AlgebraicClosure K),
  Membership.mem (γ := Subalgebra K (AlgebraicClosure K))
      (IntermediateField.toSubalgebra
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
      x_1 ∧
    (f : (a : AlgebraicClosure K) → AlgebraicClosure K) x_1 = x
Tactic: rw [← IntermediateField.mem_toSubalgebra, IntermediateField.toSubalgebra_map,
    Subalgebra.mem_map] at hx
Cleared hypotheses: hx
-- 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
x : AlgebraicClosure K
hx :
  ∃ (x_1 : AlgebraicClosure K),
    Membership.mem (γ := Subalgebra K (AlgebraicClosure K))
        (IntermediateField.toSubalgebra
          (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}))
        x_1 ∧
      (f : (a : AlgebraicClosure K) → AlgebraicClosure K) x_1 = x
⊢ Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
have right : ∀ (y : AlgebraicClosure K)
  (hy :
    Membership.mem (γ := Subalgebra K (AlgebraicClosure K))
      (IntermediateField.toSubalgebra
        (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)
Tactic: obtain ⟨y, hy, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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 (γ := Subalgebra K (AlgebraicClosure K))
    (IntermediateField.toSubalgebra (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 hy₁ : Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
  (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
Tactic: rw [IntermediateField.mem_toSubalgebra] at hy
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 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)
have right : ∀ (n : ℕ) (hn : n ∈ S) (h1 : n ≠ 0) (h2 : x ^ n = 1),
  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: obtain ⟨n, hn, h1, h2⟩ := hx
Cleared hypotheses: hx
-- 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 x : AlgebraicClosure K
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
⊢ 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)
have right : Membership.mem (α := AlgebraicClosure K) (γ := Set (AlgebraicClosure K))
  {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
  ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
Tactic: apply IntermediateField.subset_adjoin
-- 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 x : AlgebraicClosure K
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
⊢ Membership.mem (α := AlgebraicClosure K) (γ := Set (AlgebraicClosure K))
    {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
have right : HPow.hPow (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K) n = 1
Tactic: use n, hn, h1
-- 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 x : AlgebraicClosure K
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
⊢ HPow.hPow (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K) n = 1
have right : Eq (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) (x ^ n) : AlgebraicClosure K)
  (1 : AlgebraicClosure K)
Tactic: rw [← map_pow, ← map_one f, h2]
-- 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 x : AlgebraicClosure K
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
right :
  Eq (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) (x ^ n) : AlgebraicClosure K)
    (1 : AlgebraicClosure K)
⊢ HPow.hPow (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K) n = 1
have right₁ : Eq (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) (x ^ n) : AlgebraicClosure K)
  ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) 1 : AlgebraicClosure K)
Tactic: rw [← map_pow, ← map_one f, h2]
-- 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 x : AlgebraicClosure K
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : x ^ n = 1
right :
  Eq (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) (x ^ n) : AlgebraicClosure K)
    (1 : AlgebraicClosure K)
right₁ :
  Eq (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) (x ^ n) : AlgebraicClosure K)
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) 1 : AlgebraicClosure K)
⊢ HPow.hPow (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K) n = 1
have right₂ : Eq (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) 1)
  ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) 1)
Tactic: rw [← map_pow, ← map_one f, h2]
-- 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
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)
have h : Eq (α := AlgebraicClosure K)
  ((f : (a : AlgebraicClosure K) → AlgebraicClosure K)
      ((algebraMap K (AlgebraicClosure K) : (a : K) → AlgebraicClosure K) x) :
    AlgebraicClosure K)
  ((algebraMap K (AlgebraicClosure K) : (a : K) → AlgebraicClosure K) x : AlgebraicClosure K)
Tactic: convert! IntermediateField.algebraMap_mem _ x
-- 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_1 x y : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
hy :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
ihx :
  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)
ihy :
  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)
⊢ 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 + y) : AlgebraicClosure K)
have right : Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
  (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
  (HAdd.hAdd (α := AlgebraicClosure K) (β := AlgebraicClosure K)
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K))
Tactic: rw [map_add]
-- 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_1 x y : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
hy :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
ihx :
  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)
ihy :
  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)
⊢ 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 * y) : AlgebraicClosure K)
have right : Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
  (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
  (HMul.hMul (α := AlgebraicClosure K) (β := AlgebraicClosure K)
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K))
Tactic: rw [map_mul]
-- 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 x : AlgebraicClosure K
hx :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x
ihx :
  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) x⁻¹ : AlgebraicClosure K)
have right : 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: rw [map_inv₀]