awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
this : NeZero n₁
obtain : ∀ (ζ₂ : ↥C₂) (hζ₂ : IsPrimitiveRoot ζ₂ n₂), C₁ ≤ C₂
⊢ C₁ ≤ C₂

Tactic:
obtain ⟨ζ₂, hζ₂⟩ := h₂.1 rfl (NeZero.ne n₂)

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot, rfl, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
⊢ IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂

Tactic:
replace hζ₂ := hζ₂.map_of_injective (FaithfulSMul.algebraMap_injective C₂ B)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
h : n₁ ∣ n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
obtain : ∀ (d : ℕ) (hd : n₂ = n₁ * d), C₁ ≤ C₂
⊢ C₁ ≤ C₂

Tactic:
obtain ⟨d, hd⟩ := h
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
d : ℕ
hd : n₂ = n₁ * d
rwa : n₂ = n₁ * d
a b : ℕ
rwa₁ : n₂ = n₁ * d
a₁ b₁ : ℕ
rwa₂ : n₂ = n₁ * d
a₂ b₂ : ℕ
rwa₃ : n₂ = n₁ * d
a₃ b₃ : ℕ
⊢ n₂ = d * n₁

Tactic:
rwa [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
d : ℕ
hd : n₂ = n₁ * d
⊢ IsPrimitiveRoot (HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) d) n₁

Tactic:
have hζ₁ := IsPrimitiveRoot.pow n₂.pos_of_neZero hζ₂ (by rwa [mul_comm])
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₂
this : NeZero n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
d : ℕ
hd : n₂ = n₁ * d
hζ₁ : IsPrimitiveRoot (HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) d) n₁
⊢ C₁ ≤ C₂

Tactic:
simpa [(isCyclotomicExtension_singleton_iff_eq_adjoin n₁ C₁ hζ₁).mp h₁,
    (isCyclotomicExtension_singleton_iff_eq_adjoin n₂ C₂ hζ₂).mp h₂] using
    adjoin_le <| Set.singleton_subset_iff.mpr <|
      Subalgebra.pow_mem _ (self_mem_adjoin_singleton A _) _

Premises used: Iff.mpr, Set.singleton_subset_iff, isCyclotomicExtension_singleton_iff_eq_adjoin, Subalgebra.pow_mem, Algebra.adjoin_le, Iff.mp, Algebra.self_mem_adjoin_singleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
obtain : ∀ (ζ₁ : ↥C₁) (hζ₁ : IsPrimitiveRoot ζ₁ n₁), IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)

Tactic:
obtain ⟨ζ₁, hζ₁⟩ := h₁.1 rfl (NeZero.ne n₁)

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot, rfl, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
obtain : ∀ (ζ₂ : ↥C₂) (hζ₂ : IsPrimitiveRoot ζ₂ n₂), IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)

Tactic:
obtain ⟨ζ₂, hζ₂⟩ := h₂.1 rfl (NeZero.ne n₂)

Premises used: IsCyclotomicExtension.exists_isPrimitiveRoot, rfl, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
hζ₁ : IsPrimitiveRoot ζ₁ n₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
⊢ IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁

Tactic:
replace hζ₁ := hζ₁.map_of_injective (FaithfulSMul.algebraMap_injective C₁ B)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
⊢ IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂

Tactic:
replace hζ₂ := hζ₂.map_of_injective (FaithfulSMul.algebraMap_injective C₂ B)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
⊢ IsPrimitiveRoot
    (HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
      HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)

Tactic:
have hζ := hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
hζ :
  IsPrimitiveRoot
    (HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
      HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
rw :
  IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A
    ↥A[HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
          HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂)]
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A ↥(C₁ ⊔ C₂)

Tactic:
rw [sup_comm, (isCyclotomicExtension_singleton_iff_eq_adjoin n₁ C₁ hζ₁).mp h₁,
    (isCyclotomicExtension_singleton_iff_eq_adjoin n₂ C₂ hζ₂).mp h₂, ← adjoin_union,
    Set.union_singleton, hζ₁.adjoin_pair_eq A hζ₂ (NeZero.ne _) (NeZero.ne _) hζ]

Premises used: Algebra.adjoin_union, IsPrimitiveRoot.adjoin_pair_eq, isCyclotomicExtension_singleton_iff_eq_adjoin, sup_comm, Iff.mp, Set.union_singleton, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
hζ :
  IsPrimitiveRoot
    (HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
      HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
⊢ NeZero (n₁.lcm n₂)

Tactic:
have : NeZero (n₁.lcm n₂) := ⟨Nat.lcm_ne_zero (NeZero.ne _) (NeZero.ne _)⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
hζ :
  IsPrimitiveRoot
    (HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
      HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
this : NeZero (n₁.lcm n₂)
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A
    ↥A[HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
          HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂)]

Tactic:
(hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)).adjoin_isCyclotomicExtension A

Premises used: IsPrimitiveRoot.pow_mul_pow_lcm, Set.Mem, setOf, IsPrimitiveRoot.adjoin_isCyclotomicExtension, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : IsDomain B
n₁ n₂ : ℕ
C₁ C₂ : Subalgebra A B
h₁ : IsCyclotomicExtension.{u, v} {n₁} A ↥C₁
h₂ : IsCyclotomicExtension.{u, v} {n₂} A ↥C₂
inst_4 : NeZero n₁
inst_5 : NeZero n₂
ζ₁ : ↥C₁
ζ₂ : ↥C₂
hζ₁ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) n₁
hζ₂ : IsPrimitiveRoot (M := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) n₂
hζ :
  IsPrimitiveRoot
    (HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
      HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂))
    (n₁.lcm n₂)
this : NeZero (n₁.lcm n₂)
⊢ IsCyclotomicExtension.{u, v} {n₁.lcm n₂} A
    ↥A[HPow.hPow (α := B) ((algebraMap (↥C₁) B : (a : ↥C₁) → B) ζ₁ : B) (n₁ / n₁.factorizationLCMLeft n₂) *
          HPow.hPow (α := B) ((algebraMap (↥C₂) B : (a : ↥C₂) → B) ζ₂ : B) (n₂ / n₁.factorizationLCMRight n₂)]

Tactic:
exact (hζ₁.pow_mul_pow_lcm hζ₂ (NeZero.ne n₁) (NeZero.ne n₂)).adjoin_isCyclotomicExtension A

Premises used: IsPrimitiveRoot.pow_mul_pow_lcm, IsPrimitiveRoot.adjoin_isCyclotomicExtension, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
F : IntermediateField K L
ζ : L
hζ : IsPrimitiveRoot ζ n
rw : IsCyclotomicExtension.{w, z} {n} K ↥F ↔ F.toSubalgebra = K[ζ]
⊢ IsCyclotomicExtension.{w, z} {n} K ↥F ↔ F = K⟮ζ⟯

Tactic:
rw [← toSubalgebra_inj, adjoin_simple_toSubalgebra_of_isAlgebraic
    (hζ.isIntegral (NeZero.pos _)).tower_top.isAlgebraic]

Premises used: IsIntegral.isAlgebraic, IsPrimitiveRoot.isIntegral, IntermediateField.adjoin_simple_toSubalgebra_of_isAlgebraic, NeZero.pos, IsIntegral.tower_top, IntermediateField.toSubalgebra_inj
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
F : IntermediateField K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension.{w, z} {n} K ↥F ↔ F.toSubalgebra = K[ζ]

Tactic:
_root_.isCyclotomicExtension_singleton_iff_eq_adjoin n F.toSubalgebra hζ

Premises used: Set.Mem, isCyclotomicExtension_singleton_iff_eq_adjoin, IntermediateField.toSubalgebra
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
K : Type w
L : Type z
inst_1 : Field K
inst_2 : Field L
inst_3 : Algebra K L
F : IntermediateField K L
ζ : L
hζ : IsPrimitiveRoot ζ n
⊢ IsCyclotomicExtension.{w, z} {n} K ↥F ↔ F.toSubalgebra = K[ζ]

Tactic:
exact _root_.isCyclotomicExtension_singleton_iff_eq_adjoin n F.toSubalgebra hζ

Premises used: isCyclotomicExtension_singleton_iff_eq_adjoin, IntermediateField.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
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} S K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} S K ↥F₂
⊢ F₁ = F₂

Tactic:
toSubalgebra_inj.mp <| _root_.IsCyclotomicExtension.eq S F₁.toSubalgebra F₂.toSubalgebra

Premises used: IsCyclotomicExtension.eq, Iff.mp, IntermediateField.toSubalgebra_inj, IntermediateField.toSubalgebra
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} {n₁} K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} {n₂} K ↥F₂
inst_3 : NeZero n₂
h : n₁ ∣ n₂
⊢ F₁ ≤ F₂

Tactic:
toSubalgebra_le_toSubalgebra.mp <|
    IsCyclotomicExtension.le_of_dvd n₁ n₂ F₁.toSubalgebra F₂.toSubalgebra h

Premises used: IsCyclotomicExtension.le_of_dvd, Iff.mp, IntermediateField.toSubalgebra_le_toSubalgebra, IntermediateField.toSubalgebra
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} {n₁} K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} {n₂} K ↥F₂
inst_3 : NeZero n₂
h : n₁ ∣ n₂
⊢ F₁ ≤ F₂

Tactic:
exact toSubalgebra_le_toSubalgebra.mp <|
    IsCyclotomicExtension.le_of_dvd n₁ n₂ F₁.toSubalgebra F₂.toSubalgebra h

Premises used: IsCyclotomicExtension.le_of_dvd, Iff.mp, IntermediateField.toSubalgebra_le_toSubalgebra, IntermediateField.toSubalgebra
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} {n₁} K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} {n₂} K ↥F₂
inst_3 : NeZero n₁
inst_4 : NeZero n₂
⊢ FiniteDimensional.{w, z} K ↥F₁

Tactic:
have : FiniteDimensional K F₁ := IsCyclotomicExtension.finite_of_singleton n₁ K F₁
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} {n₁} K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} {n₂} K ↥F₂
inst_3 : NeZero n₁
inst_4 : NeZero n₂
this : FiniteDimensional.{w, z} K ↥F₁
⊢ IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁.toSubalgebra ⊔ F₂.toSubalgebra)

Tactic:
have := IsCyclotomicExtension.lcm_sup n₁ n₂ F₁.toSubalgebra F₂.toSubalgebra
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
n₁ n₂ : ℕ
F₁ F₂ : IntermediateField K L
h₁ : IsCyclotomicExtension.{w, z} {n₁} K ↥F₁
h₂ : IsCyclotomicExtension.{w, z} {n₂} K ↥F₂
inst_3 : NeZero n₁
inst_4 : NeZero n₂
this_1 : FiniteDimensional.{w, z} K ↥F₁
this : IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁.toSubalgebra ⊔ F₂.toSubalgebra)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁ ⊔ F₂).toSubalgebra),
    IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)
⊢ IsCyclotomicExtension.{w, z} {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)

Tactic:
rwa [← sup_toSubalgebra_of_left] at this

Premises used: IntermediateField.sup_toSubalgebra_of_left
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
obtain :
  ∀ (m : ℤ)
    (hm :
      ∀ (g_1 : ↥(rootsOfUnity n L)),
        (MulEquiv.toMonoidHom (MulEquiv.restrictRootsOfUnity (↑g : L ≃* L) n) :
              (a : ↥(rootsOfUnity n L)) → ↥(rootsOfUnity n L))
            g_1 =
          g_1 ^ m),
    ∃ (m : ℤ), ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ m) : L)
⊢ ∃ (m : ℤ), ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ m) : L)

Tactic:
obtain ⟨m, hm⟩ := MonoidHom.map_cyclic ((g : L ≃* L).restrictRootsOfUnity n).toMonoidHom

Premises used: MonoidHom.map_cyclic, MulEquiv.toMonoidHom, MulEquiv.restrictRootsOfUnity, MulEquivClass.toMulEquiv
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
m : ℤ
hm :
  ∀ (g_1 : ↥(rootsOfUnity n L)),
    (MulEquiv.toMonoidHom (MulEquiv.restrictRootsOfUnity (↑g : L ≃* L) n) :
          (a : ↥(rootsOfUnity n L)) → ↥(rootsOfUnity n L))
        g_1 =
      g_1 ^ m
⊢ ∃ (m : ℤ), ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ m) : L)

Tactic:
⟨m, fun t ↦ Units.ext_iff.1 <| SetCoe.ext_iff.2 <| hm t⟩

Premises used: Iff.mpr, Units.ext_iff, Exists.intro, Iff.mp, SetCoe.ext_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
m : ℤ
hm :
  ∀ (g_1 : ↥(rootsOfUnity n L)),
    (MulEquiv.toMonoidHom (MulEquiv.restrictRootsOfUnity (↑g : L ≃* L) n) :
          (a : ↥(rootsOfUnity n L)) → ↥(rootsOfUnity n L))
        g_1 =
      g_1 ^ m
⊢ ∃ (m : ℤ), ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ m) : L)

Tactic:
exact ⟨m, fun t ↦ Units.ext_iff.1 <| SetCoe.ext_iff.2 <| hm t⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
n : ℕ
inst_2 : NeZero n
g : L ≃+* L
⊢ ∃ (m : ℤ),
    ∀ (t : Lˣ), Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity n L) t → (g : (a : L) → L) (↑t : L) = (↑(t ^ m) : L)

Tactic:
simpa using rootsOfUnity.integer_power_of_ringEquiv n g

Premises used: rootsOfUnity.integer_power_of_ringEquiv
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
n : ℕ
inst_2 : NeZero n
⊢ ∀ (t : ↥(rootsOfUnity n L)), (g : (a : L) → L) (↑(↑t : Lˣ) : L) = (↑((↑t : Lˣ) ^ aux g n) : L)

Tactic:
(rootsOfUnity.integer_power_of_ringEquiv n g).choose_spec

Premises used: Exists.choose_spec, modularCyclotomicCharacter.aux, rootsOfUnity.integer_power_of_ringEquiv
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
i k : ℕ
hi : k ≤ i
obtain : ∀ (i : ℕ) (hi : k ≤ k + i), HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ i) - aux g (p ^ k)

Tactic:
obtain ⟨i, rfl⟩ := exists_add_of_le hi

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
obtain :
  ∀ (ζ : L) (hζ : IsPrimitiveRoot ζ (p ^ (k + i))), HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)
⊢ HPow.hPow (α := ℤ) (↑p : ℤ) k ∣ aux g (p ^ (k + i)) - aux g (p ^ k)

Tactic:
obtain ⟨ζ, hζ⟩ := HasEnoughRootsOfUnity.exists_primitiveRoot L (p ^ (k + i))

Premises used: HasEnoughRootsOfUnity.exists_primitiveRoot, HPow.hPow, HAdd.hAdd
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
⊢ IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)

Tactic:
have h := hζ.pow (a := p ^ i) (Nat.pos_of_neZero _) (Nat.pow_add' _ _ _)
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
huv : (↑⋯.unit : L) = (↑(⋯.unit ^ p ^ i) : L)
⊢ ⋯.unit = ⋯.unit ^ p ^ i

Tactic:
ext
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
⊢ (↑⋯.unit : L) = (↑(⋯.unit ^ p ^ i) : L)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
⊢ ⋯.unit = ⋯.unit ^ p ^ i

Tactic:
have h_unit : (h.isUnit NeZero.out).unit =
      (hζ.isUnit NeZero.out).unit ^ (p ^ i) := by ext; rfl
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
⊢ (g : (a : L) → L)
      (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) :
        L) =
    (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) ^
          aux g (p ^ (k + i))) :
      L)

Tactic:
have H₁ := aux_spec g (p ^ (k + i))
    ⟨_, (hζ.isUnit_unit NeZero.out).mem_rootsOfUnity⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
Goal:
L : Type u
inst : CommRing L
inst_1 : IsDomain L
g : L ≃+* L
p : ℕ
inst_2 : Fact (Nat.Prime p)
inst_3 : ∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)
k i : ℕ
hi : k ≤ k + i
ζ : L
hζ : IsPrimitiveRoot ζ (p ^ (k + i))
h : IsPrimitiveRoot (ζ ^ p ^ i) (p ^ k)
h_unit : ⋯.unit = ⋯.unit ^ p ^ i
H₁ :
  (g : (a : L) → L)
      (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) :
        L) =
    (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ (k + i)) L) x) ⋯.unit
                ⋯) :
            Lˣ) ^
          aux g (p ^ (k + i))) :
      L)
⊢ (g : (a : L) → L)
      (↑(↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) x) ⋯.unit ⋯) :
            Lˣ) :
        L) =
    (↑((↑(Subtype.mk (p := fun (x : Lˣ) ↦ Membership.mem (γ := Subgroup Lˣ) (rootsOfUnity (p ^ k) L) x) ⋯.unit ⋯) :
            Lˣ) ^
          aux g (p ^ k)) :
      L)

Tactic:
have H₂ := aux_spec g (p ^ k)
    ⟨_, (h.isUnit_unit NeZero.out).mem_rootsOfUnity⟩