awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
rw : IsPrimitiveRoot hζ.toInteger (n₁ * n₂)
⊢ IsPrimitiveRoot hζ.toInteger (n₁.lcm n₂)

Tactic:
rw [Nat.Coprime.lcm_eq_mul h]

Premises used: Nat.Coprime.lcm_eq_mul
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
⊢ IsPrimitiveRoot hζ.toInteger (n₁ * n₂)

Tactic:
toInteger_isPrimitiveRoot hζ

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
⊢ IsPrimitiveRoot hζ.toInteger (n₁ * n₂)

Tactic:
exact toInteger_isPrimitiveRoot hζ

Premises used: IsPrimitiveRoot.toInteger_isPrimitiveRoot
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
⊢ F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤

Tactic:
simp [← sup_toSubalgebra_of_left, htop]

Premises used: IntermediateField.sup_toSubalgebra_of_left
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
⊢ IsCoprime.{u} (R := Ideal (𝓞 K))
    (Ideal.map (R := 𝓞 ↥F₁) (F := 𝓞 ↥F₁ →+* 𝓞 K) (algebraMap (𝓞 ↥F₁) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₁)))
    (Ideal.map (R := 𝓞 ↥F₂) (F := 𝓞 ↥F₂ →+* 𝓞 K) (algebraMap (𝓞 ↥F₂) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₂)))

Tactic:
isCoprime_differentIdeal_of_isCoprime_discr _ h_cpr

Premises used: NumberField.isCoprime_differentIdeal_of_isCoprime_discr
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
inst_2 : NumberField K
F₁ F₂ : IntermediateField ℚ K
n₁ n₂ : ℕ
inst_3 : NeZero n₁
inst_4 : NeZero n₂
inst_5 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥F₁
inst_6 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥F₂
ζ₁ : ↥F₁
hζ₁_1 : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁_1.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂_1 : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂_1.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
h_disj : F₁.LinearDisjoint ↥F₂
hζ₁ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁
hζ₂ : IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂
⊢ IsCoprime.{u} (R := Ideal (𝓞 K))
    (Ideal.map (R := 𝓞 ↥F₁) (F := 𝓞 ↥F₁ →+* 𝓞 K) (algebraMap (𝓞 ↥F₁) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₁)))
    (Ideal.map (R := 𝓞 ↥F₂) (F := 𝓞 ↥F₂ →+* 𝓞 K) (algebraMap (𝓞 ↥F₂) (𝓞 K)) (differentIdeal ℤ (𝓞 ↥F₂)))

Tactic:
exact isCoprime_differentIdeal_of_isCoprime_discr _ h_cpr

Premises used: NumberField.isCoprime_differentIdeal_of_isCoprime_discr
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ n
⊢ NumberField K

Tactic:
haveI : NumberField K := IsCyclotomicExtension.numberField {n} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (R := ℕ) 0
hK : IsCyclotomicExtension {0} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ 0
this : NumberField K
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤

Tactic:
(neZero_zero_iff_false.mp hn).elim

Premises used: False.elim, neZero_zero_iff_false, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (R := ℕ) 0
hK : IsCyclotomicExtension {0} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ 0
this : NumberField K
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤

Tactic:
exact (neZero_zero_iff_false.mp hn).elim

Premises used: False.elim, neZero_zero_iff_false, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ k)
this : NumberField K
⊢ Fact (Nat.Prime p)

Tactic:
have : Fact (p.Prime) := ⟨hp⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
p k : ℕ
hp : Nat.Prime p
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (p ^ k)
hK : IsCyclotomicExtension {p ^ k} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ k)
this_1 : NumberField K
this : Fact (Nat.Prime p)
prime_pow : Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ℤ[hζ.integralPowerBasisOfPrimePow.gen]
prime_pow₁ prime_pow₂ : Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ℤ[hζ.toInteger]
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤

Tactic:
rw [← hζ.integralPowerBasisOfPrimePow.adjoin_gen_eq_top, hζ.integralPowerBasisOfPrimePow_gen]

Premises used: IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, IsPrimitiveRoot.integralPowerBasisOfPrimePow, PowerBasis.adjoin_gen_eq_top
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₁) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this : NumberField K
⊢ NeZero n₁

Tactic:
have : NeZero n₁ := NeZero.of_gt hn₁
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₁) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this : NeZero n₁
⊢ NeZero n₂

Tactic:
have : NeZero n₂ := NeZero.of_gt hn₂
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₁) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this : NeZero n₂
rw rw₁ : n₂ * n₁ = n₂ * n₁
⊢ n₁ * n₂ = n₂ * n₁

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₁) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this : NeZero n₂
⊢ IsPrimitiveRoot (ζ ^ n₂) n₁

Tactic:
have hζ₁ := hζ.pow (NeZero.pos _) (a := n₂) (b := n₁) (by rw [mul_comm])
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₁) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this : NeZero n₂
hζ₁ : IsPrimitiveRoot (ζ ^ n₂) n₁
⊢ IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯

Tactic:
have := hζ₁.intermediateField_adjoin_isCyclotomicExtension ℚ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₁) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
hζ₁ : IsPrimitiveRoot (ζ ^ n₂) n₁
this : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
⊢ IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁

Tactic:
replace hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₁
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₁ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₁) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
⊢ Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤

Tactic:
replace hK₁ := @hK₁ ℚ⟮ζ ^ n₂⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₁ (of_intermediateField _)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
⊢ IsPrimitiveRoot (ζ ^ n₁) n₂

Tactic:
have hζ₂ := hζ.pow (NeZero.pos _) (a := n₁) (b := n₂) rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
hζ₂ : IsPrimitiveRoot (ζ ^ n₁) n₂
⊢ IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯

Tactic:
have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
hζ₂ : IsPrimitiveRoot (ζ ^ n₁) n₂
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
⊢ IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂

Tactic:
replace hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
hK₂ :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K] {ζ : K}
    (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
⊢ Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤

Tactic:
replace hK₂ := @hK₂ ℚ⟮ζ ^ n₁⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₂ (of_intermediateField _)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
⊢ IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤

Tactic:
have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
rw : IsCyclotomicExtension.{0, u} {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
⊢ IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)

Tactic:
rw [← Nat.Coprime.lcm_eq_mul h]

Premises used: Nat.Coprime.lcm_eq_mul
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension.{0, u} {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)

Tactic:
isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯

Premises used: Set.Mem, Rat, IntermediateField.isCyclotomicExtension_lcm_sup, HPow.hPow, IntermediateField.adjoin, RingHom.codRestrict, Rat.castHom, Singleton.singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension.{0, u} {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)

Tactic:
exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯

Premises used: Rat, IntermediateField.isCyclotomicExtension_lcm_sup, HPow.hPow, IntermediateField.adjoin, Singleton.singleton
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n₁ n₂ : ℕ
hn₁ : 1 < n₁
hn₂ : 1 < n₂
h : n₁.Coprime n₂
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero (n₁ * n₂)
hK : IsCyclotomicExtension {n₁ * n₂} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
hζ₁ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
this : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
⊢ IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)

Tactic:
have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯