awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 :
  {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)
⊢ 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:
rw [IntermediateField.adjoin_le_iff]

Premises used: IntermediateField.adjoin_le_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}) ⊤
y : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
⊢ HPow.hPow (α := M) ((i : (a : L) → M) y : M) n = 1

Tactic:
simpa using congrArg i h2

Premises used: congrArg, DFunLike.coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}) ⊤
y : L
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
h2 : y ^ n = 1
⊢ Membership.mem (α := M) (↑(IntermediateField.adjoin K {x : M | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) : Set M)
    ((i : (a : L) → M) y : M)

Tactic:
exact IntermediateField.subset_adjoin K _ ⟨n, hn, h1, by simpa using congrArg i h2⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ NeZero n

Tactic:
have : NeZero n := ⟨h1⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ 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

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ 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 ⟨m, -, rfl⟩ := (hy.map_of_injective i.injective).eq_pow_of_pow_eq_one h2

Premises used: RingHom.injective, AlgHom.toRingHom, IsPrimitiveRoot.map_of_injective, IsPrimitiveRoot.eq_pow_of_pow_eq_one, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}) ⊤
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
this : NeZero n
y : L
hy : IsPrimitiveRoot y n
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:
pow_mem (IntermediateField.subset_adjoin K (i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m

Premises used: Set.Mem, setOf, Membership.mem, Exists, Ne, IntermediateField.subset_adjoin, And, HPow.hPow, And.intro, Exists.intro, pow_mem, Set.image, OfNat.ofNat, Eq, IsPrimitiveRoot.pow_eq_one, DFunLike.coe, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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}) ⊤
n : ℕ
hn : n ∈ S
h1 : n ≠ 0
this : NeZero n
y : L
hy : IsPrimitiveRoot y n
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:
exact pow_mem (IntermediateField.subset_adjoin K (i '' {x : L | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ⟨y, ⟨n, hn, h1, hy.pow_eq_one⟩, rfl⟩) m

Premises used: setOf, Membership.mem, Exists, Ne, IntermediateField.subset_adjoin, And, HPow.hPow, And.intro, Exists.intro, pow_mem, Set.image, OfNat.ofNat, Eq, IsPrimitiveRoot.pow_eq_one, DFunLike.coe, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
rw : Algebra.IsSeparable K L ∧ Normal K L
⊢ IsGalois K L

Tactic:
rw [isGalois_iff]

Premises used: isGalois_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
right : Normal K L
⊢ Algebra.IsSeparable K L ∧ Normal K L

Tactic:
use isSeparable S K L

Premises used: IsCyclotomicExtension.isSeparable
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
right : ∀ (i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})), Normal K L
⊢ Normal K L

Tactic:
obtain ⟨i⟩ := nonempty_algEquiv_adjoin_of_isSepClosed S K L (AlgebraicClosure K)

Premises used: AlgebraicClosure, IsCyclotomicExtension.nonempty_algEquiv_adjoin_of_isSepClosed
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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})
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}
⊢ Normal K L

Tactic:
rw [i.transfer_normal, IntermediateField.normal_iff_forall_map_le]

Premises used: AlgEquiv.transfer_normal, IntermediateField.normal_iff_forall_map_le
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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})
⊢ ∃ (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

Premises used: IntermediateField.toSubalgebra_map, Subalgebra.mem_map, IntermediateField.mem_toSubalgebra
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x

Tactic:
obtain ⟨y, hy, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 (γ := 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

Premises used: IntermediateField.mem_toSubalgebra
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ 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
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 :
  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)
⊢ 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:
apply IntermediateField.subset_adjoin

Premises used: IntermediateField.subset_adjoin
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 :
  HPow.hPow (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K) 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)

Tactic:
use n, hn, h1
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
right₂ right₃ :
  Eq (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) 1)
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) 1)
⊢ HPow.hPow (α := AlgebraicClosure K) ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K) n = 1

Tactic:
rw [← map_pow, ← map_one f, h2]

Premises used: map_pow, map_one
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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})
    ((algebraMap K (AlgebraicClosure K) : (a : K) → AlgebraicClosure K) x : AlgebraicClosure K)

Tactic:
IntermediateField.algebraMap_mem _ x

Premises used: IntermediateField.algebraMap_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
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)
⊢ 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:
convert! IntermediateField.algebraMap_mem _ x

Premises used: IntermediateField.algebraMap_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ 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:
AlgHom.commutes _ x

Premises used: AlgHom.commutes
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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
⊢ 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:
exact AlgHom.commutes _ x

Premises used: AlgHom.commutes
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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)
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))
⊢ 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)

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 (γ := 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:
add_mem ihx ihy

Premises used: AddMemClass.add_mem
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
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 (γ := 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:
exact add_mem ihx ihy

Premises used: AddMemClass.add_mem