awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this_1 : NumberField K
this_2 : NeZero n₁
this_3 : NeZero n₂
ζ : K := zeta (n₁ * n₂) ℚ K
hζ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K) (n₁ * n₂)
hζ₁ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₂) n₁
this_4 : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₂⟯
hζ₁' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
hK₁ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯).natAbs = n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))
hζ₂ : IsPrimitiveRoot (zeta (n₁ * n₂) ℚ K ^ n₁) n₂
this_5 : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮zeta (n₁ * n₂) ℚ K ^ n₁⟯
hζ₂' : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
hK₂ : (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯).natAbs = n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1))
this_6 : IsGalois.{0, u} ℚ ↥ℚ⟮ζ ^ n₂⟯
h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
h_cpr : IsCoprime (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₂⟯) (NumberField.discr.{u} ↥ℚ⟮ζ ^ n₁⟯)
h_dsj : IntermediateField.LinearDisjoint (E := K) ℚ⟮ζ ^ n₂⟯ ↥ℚ⟮ζ ^ n₁⟯
h_div₁ : ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1)) ∣ n₁ ^ φ n₁
h_div₂ : ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)) ∣ n₂ ^ φ n₂
this : ∀ {n p : ℕ} (hp : p ∈ n.primeFactors), p - 1 ∣ φ n
e_a :
  n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₂ * φ n₁) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₂ * φ n₁ / (x - 1))) =
    n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₁ * φ n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
e_a₁ e_a₂ :
  n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₁ * φ n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1))) =
    n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₁ * φ n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
⊢ n₁ ^ (φ n₁ * φ n₂) * n₂ ^ (φ n₂ * φ n₁) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₂ * φ n₁ / (x - 1))) =
    (n₁ * n₂) ^ (φ n₁ * φ n₂) /
      HMul.hMul (α := ℕ) (∏ x ∈ n₁.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))
        (∏ x ∈ n₂.primeFactors, x ^ (φ n₁ * φ n₂ / (x - 1)))

Tactic:
rw [mul_pow, mul_comm n₂.totient]

Premises used: Nat.totient, mul_comm, mul_pow
-- 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
⊢ NumberField K

Tactic:
have : NumberField K := IsCyclotomicExtension.numberField {n} ℚ K
-- 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
this : NumberField K
rw : (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ) ∣ HPow.hPow (α := ℤ) (↑n : ℤ) (φ n)
⊢ (NumberField.discr K).natAbs = n ^ φ n / ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))

Tactic:
rw [discr n K, Int.natAbs_mul, Int.natAbs_pow, Int.natAbs_neg, Int.natAbs_one, one_pow, one_mul,
    Int.natAbs_ediv_of_dvd, Int.natAbs_pow, Int.natAbs_natCast, Int.natAbs_natCast]

Premises used: one_pow, Int.natAbs_one, Int.natAbs_mul, Int.natAbs_ediv_of_dvd, IsCyclotomicExtension.Rat.discr, Int.natAbs_pow, Int.natAbs_natCast, Int.natAbs_neg, one_mul
-- 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
this : NumberField K
rw : ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n
⊢ (↑(∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1))) : ℤ) ∣ HPow.hPow (α := ℤ) (↑n : ℤ) (φ n)

Tactic:
rw [← Nat.cast_pow, Int.natCast_dvd_natCast]

Premises used: Nat.cast_pow, Int.natCast_dvd_natCast
-- 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
this : NumberField K
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n

Tactic:
Nat.prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _)

Premises used: NeZero.pos, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- 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
this : NumberField K
⊢ ∏ p ∈ n.primeFactors, p ^ (φ n / (p - 1)) ∣ n ^ φ n

Tactic:
exact Nat.prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _)

Premises used: NeZero.pos, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
rw :
  (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
    (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
⊢ IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)

Tactic:
rw [Int.isCoprime_iff_nat_coprime, natAbs_discr n₁ F₁, natAbs_discr n₂ F₂]

Premises used: Int.isCoprime_iff_nat_coprime, Membership.mem, Subtype, IsCyclotomicExtension.Rat.natAbs_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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
    (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))

Tactic:
Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))

Premises used: NeZero.pos, Nat.Coprime.coprime_div_left, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
refine : (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))
⊢ (n₁ ^ φ n₁ / ∏ p ∈ n₁.primeFactors, p ^ (φ n₁ / (p - 1))).Coprime
    (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))

Tactic:
refine Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))

Premises used: NeZero.pos, Nat.Coprime.coprime_div_left, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))

Tactic:
Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))

Premises used: Nat.Coprime.coprime_div_right, NeZero.pos, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
refine : (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂)
⊢ (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂ / ∏ p ∈ n₂.primeFactors, p ^ (φ n₂ / (p - 1)))

Tactic:
refine Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))

Premises used: Nat.Coprime.coprime_div_right, NeZero.pos, Nat.prod_primeFactors_pow_totient_ediv_dvd
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂)

Tactic:
Coprime.pow_left _ (Coprime.pow_right _ h)

Premises used: Nat.Coprime.pow_right, Nat.Coprime.pow_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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ (n₁ ^ φ n₁).Coprime (n₂ ^ φ n₂)

Tactic:
exact Coprime.pow_left _ (Coprime.pow_right _ h)

Premises used: Nat.Coprime.pow_right, Nat.Coprime.pow_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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
⊢ IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)

Tactic:
have h_cpr : IsCoprime (NumberField.discr F₁) (NumberField.discr F₂) := by
    rw [Int.isCoprime_iff_nat_coprime, natAbs_discr n₁ F₁, natAbs_discr n₂ F₂]
    refine Coprime.coprime_div_left ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
    refine Coprime.coprime_div_right ?_ (prod_primeFactors_pow_totient_ediv_dvd (NeZero.pos _))
    exact Coprime.pow_left _ (Coprime.pow_right _ h)
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
⊢ IsGalois.{0, u} ℚ ↥F₁

Tactic:
have : IsGalois ℚ F₁ := IsCyclotomicExtension.isGalois {n₁} ℚ F₁
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
this : IsGalois.{0, u} ℚ ↥F₁
h₃ : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
⊢ F₁.LinearDisjoint ↥F₂

Tactic:
apply linearDisjoint_of_isGalois_isCoprime_discr

Premises used: NumberField.linearDisjoint_of_isGalois_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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
this : IsGalois.{0, u} ℚ ↥F₁
⊢ IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)

Tactic:
h_cpr

Premises used: Set.Mem
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
this : IsGalois.{0, u} ℚ ↥F₁
⊢ IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)

Tactic:
exact h_cpr
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.toInteger] ⊤
h : n₁.Coprime n₂
htop : F₁ ⊔ F₂ = ⊤
ζ : K
hζ : IsPrimitiveRoot ζ (n₁ * n₂)
h_cpr : IsCoprime (NumberField.discr.{u} ↥F₁) (NumberField.discr.{u} ↥F₂)
⊢ F₁.LinearDisjoint ↥F₂

Tactic:
have h_disj : F₁.LinearDisjoint F₂ := by
    have : IsGalois ℚ F₁ := IsCyclotomicExtension.isGalois {n₁} ℚ F₁
    apply linearDisjoint_of_isGalois_isCoprime_discr
    exact h_cpr
-- 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ζ₁ : IsPrimitiveRoot ζ₁ n₁
h₁ : Eq (α := Subalgebra ℤ (𝓞 ↥F₁)) ℤ[hζ₁.toInteger] ⊤
ζ₂ : ↥F₂
hζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.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₂
⊢ IsPrimitiveRoot hζ₁.toInteger n₁

Tactic:
replace hζ₁ : IsPrimitiveRoot hζ₁.toInteger n₁ := hζ₁.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ζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.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 hζ₁_1.toInteger n₁
⊢ IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K) n₁

Tactic:
replace hζ₁ := hζ₁.map_of_injective (FaithfulSMul.algebraMap_injective (𝓞 F₁) (𝓞 K))
-- 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ζ₂ : IsPrimitiveRoot ζ₂ n₂
h₂ : Eq (α := Subalgebra ℤ (𝓞 ↥F₂)) ℤ[hζ₂.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₁
⊢ IsPrimitiveRoot hζ₂.toInteger n₂

Tactic:
replace hζ₂ : IsPrimitiveRoot hζ₂.toInteger n₂ := hζ₂.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 hζ₂_1.toInteger n₂
⊢ IsPrimitiveRoot (M := 𝓞 K) ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K) n₂

Tactic:
replace hζ₂ := hζ₂.map_of_injective (FaithfulSMul.algebraMap_injective (𝓞 F₂) (𝓞 K))
-- 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 :
  Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger]
    ℤ[((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K),
      ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K)]
rw₁ : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
rw₂ :
  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₂)))
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤

Tactic:
rw [← IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal ℤ (𝓞 K) (𝓞 F₁)
    (𝓞 F₂) h_disj _ _ h₁ h₂, Set.image_singleton, Set.image_singleton, Set.singleton_union]

Premises used: Set.image_singleton, Membership.mem, Set.singleton_union, Subtype, Int, IsDedekindDomain.adjoin_union_eq_top_of_isCoprime_differentialIdeal, NumberField.RingOfIntegers
-- 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₂
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger]
    ℤ[((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K),
      ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K)]

Tactic:
(IsPrimitiveRoot.adjoin_pair_eq ℤ hζ₁ hζ₂ (NeZero.ne _) (NeZero.ne _) ?_).symm

Premises used: IsPrimitiveRoot.adjoin_pair_eq, Int, Eq.symm, NeZero.ne
-- 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₂
refine : IsPrimitiveRoot hζ.toInteger (n₁.lcm n₂)
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger]
    ℤ[((algebraMap (𝓞 ↥F₁) (𝓞 K) : (a : 𝓞 ↥F₁) → 𝓞 K) hζ₁_1.toInteger : 𝓞 K),
      ((algebraMap (𝓞 ↥F₂) (𝓞 K) : (a : 𝓞 ↥F₂) → 𝓞 K) hζ₂_1.toInteger : 𝓞 K)]

Tactic:
refine (IsPrimitiveRoot.adjoin_pair_eq ℤ hζ₁ hζ₂ (NeZero.ne _) (NeZero.ne _) ?_).symm

Premises used: IsPrimitiveRoot.adjoin_pair_eq, Int, Eq.symm, NeZero.ne