awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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]
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have prime_pow₁ : Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ℤ[hζ.toInteger]
Tactic: rw [← hζ.integralPowerBasisOfPrimePow.adjoin_gen_eq_top, hζ.integralPowerBasisOfPrimePow_gen]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have this₁ : NeZero n₁
Tactic: have : NeZero n₁ := NeZero.of_gt hn₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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₁
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have this₁ : NeZero n₂
Tactic: have : NeZero n₂ := NeZero.of_gt hn₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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₂
⊢ n₁ * n₂ = n₂ * n₁
have rw : n₂ * n₁ = n₂ * n₁
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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₂
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hζ₁ : IsPrimitiveRoot (ζ ^ n₂) n₁
Tactic: have hζ₁ := hζ.pow (NeZero.pos _) (a := n₂) (b := n₁) (by rw [mul_comm])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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₁
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have this₁ : IsCyclotomicExtension.{0, u} {n₁} ℚ ↥ℚ⟮ζ ^ n₂⟯
Tactic: have := hζ₁.intermediateField_adjoin_isCyclotomicExtension ℚ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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₂⟯
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hζ₂ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₂⟯) (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁
Tactic: replace hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₁
Cleared hypotheses: hζ₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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 ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hK₃ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₂⟯)) ℤ[hζ₁.toInteger] ⊤
Tactic: replace hK₁ := @hK₁ ℚ⟮ζ ^ n₂⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₁ (of_intermediateField _)
Cleared hypotheses: hK₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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] ⊤
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hζ₂ : IsPrimitiveRoot (ζ ^ n₁) n₂
Tactic: have hζ₂ := hζ.pow (NeZero.pos _) (a := n₁) (b := n₂) rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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₂
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have this₁ : IsCyclotomicExtension.{0, u} {n₂} ℚ ↥ℚ⟮ζ ^ n₁⟯
Tactic: have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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₁⟯
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hζ₃ : IsPrimitiveRoot (M := ↥ℚ⟮ζ ^ n₁⟯) (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂
Tactic: replace hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂
Cleared hypotheses: hζ₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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 ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have hK₃ : Eq (α := Subalgebra ℤ (𝓞 ↥ℚ⟮ζ ^ n₁⟯)) ℤ[hζ₂.toInteger] ⊤
Tactic: replace hK₂ := @hK₂ ℚ⟮ζ ^ n₁⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₂ (of_intermediateField _)
Cleared hypotheses: hK₂
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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] ⊤
⊢ Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
have this₁ : IsCyclotomicExtension.{0, u} {n₁ * n₂} ℚ ↥⊤
Tactic: have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
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₁⟯)
have rw : IsCyclotomicExtension.{0, u} {n₁.lcm n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯)
Tactic: rw [← Nat.Coprime.lcm_eq_mul h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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₂} ℚ ↥⊤
⊢ Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
have this₁ : 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₁⟯
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
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] ⊤
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have h_top : Eq (α := IntermediateField ℚ K) (ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) ⊤
Tactic: have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have zero : ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero (R := ℕ) 0] [hK : IsCyclotomicExtension {0} ℚ K]
  {ζ : K} (hζ : IsPrimitiveRoot ζ 0) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
Tactic: induction n using Nat.recOnPrimeCoprime generalizing K hn with
  | zero => exact (neZero_zero_iff_false.mp hn).elim
  | prime_pow p k hp =>
    have : Fact (p.Prime) := ⟨hp⟩
    rw [← hζ.integralPowerBasisOfPrimePow.adjoin_gen_eq_top, hζ.integralPowerBasisOfPrimePow_gen]
  | coprime n₁ n₂ hn₁ hn₂ h hK₁ hK₂ =>
    have : NeZero n₁ := NeZero.of_gt hn₁
    have : NeZero n₂ := NeZero.of_gt hn₂
    have hζ₁ := hζ.pow (NeZero.pos _) (a := n₂) (b := n₁) (by rw [mul_comm])
    have := hζ₁.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₁
    replace hK₁ := @hK₁ ℚ⟮ζ ^ n₂⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₁ (of_intermediateField _)
    have hζ₂ := hζ.pow (NeZero.pos _) (a := n₁) (b := n₂) rfl
    have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂
    replace hK₂ := @hK₂ ℚ⟮ζ ^ n₁⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₂ (of_intermediateField _)
    have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _
    exact adjoin_singleton_eq_top_aux K ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯ hζ₁ hK₁ hζ₂ hK₂ h h_top hζ
Cleared hypotheses: n, K, inst, inst_1, hn, hK, ζ, hζ, this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
zero :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero (R := ℕ) 0] [hK : IsCyclotomicExtension {0} ℚ K]
    {ζ : K} (hζ : IsPrimitiveRoot ζ 0) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
have prime_pow : ∀ (p k : ℕ) (hp : Nat.Prime p) {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero (p ^ k)]
  [hK : IsCyclotomicExtension {p ^ k} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ k)) (this : NumberField K),
  Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
Tactic: induction n using Nat.recOnPrimeCoprime generalizing K hn with
  | zero => exact (neZero_zero_iff_false.mp hn).elim
  | prime_pow p k hp =>
    have : Fact (p.Prime) := ⟨hp⟩
    rw [← hζ.integralPowerBasisOfPrimePow.adjoin_gen_eq_top, hζ.integralPowerBasisOfPrimePow_gen]
  | coprime n₁ n₂ hn₁ hn₂ h hK₁ hK₂ =>
    have : NeZero n₁ := NeZero.of_gt hn₁
    have : NeZero n₂ := NeZero.of_gt hn₂
    have hζ₁ := hζ.pow (NeZero.pos _) (a := n₂) (b := n₁) (by rw [mul_comm])
    have := hζ₁.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₁
    replace hK₁ := @hK₁ ℚ⟮ζ ^ n₂⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₁ (of_intermediateField _)
    have hζ₂ := hζ.pow (NeZero.pos _) (a := n₁) (b := n₂) rfl
    have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂
    replace hK₂ := @hK₂ ℚ⟮ζ ^ n₁⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₂ (of_intermediateField _)
    have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _
    exact adjoin_singleton_eq_top_aux K ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯ hζ₁ hK₁ hζ₂ hK₂ h h_top hζ
Cleared hypotheses: n, K, inst, inst_1, hn, hK, ζ, hζ, this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K
have algebraMap_injective : Function.Injective (α := ↥ℤ[ζ]) (β := K) (⇑(algebraMap (↥ℤ[ζ]) K) : (a : ↥ℤ[ζ]) → K)
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
algebraMap_injective : Function.Injective (α := ↥ℤ[ζ]) (β := K) (⇑(algebraMap (↥ℤ[ζ]) K) : (a : ↥ℤ[ζ]) → K)
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K
have isIntegral_iff : ∀ {x : K}, IsIntegral ℤ x ↔ ∃ (y : ↥ℤ[ζ]), (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x : K
⊢ IsIntegral ℤ x ↔ ∃ (y : ↥ℤ[ζ]), (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y = x
have this : Eq (α := Subalgebra ℤ K) (Subalgebra.map (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ℤ[hζ.toInteger])
  (Subalgebra.map (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ⊤)
Tactic: have := congr_arg (Subalgebra.map (IsScalarTower.toAlgHom ℤ (𝓞 K) K))
      (adjoin_singleton_eq_top hζ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
ζ : K
hcycl : IsCyclotomicExtension {n} ℚ K
hζ : IsPrimitiveRoot ζ n
x : K
this :
  Eq (α := Subalgebra ℤ K) (Subalgebra.map (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ℤ[hζ.toInteger])
    (Subalgebra.map (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K) ⊤)
⊢ IsIntegral ℤ x ↔ ∃ (y : ↥ℤ[ζ]), (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y = x
have this₁ : Eq (α := Subalgebra ℤ K) ℤ[ζ] (AlgHom.range (A := 𝓞 K) (IsScalarTower.toAlgHom ℤ (𝓞 K) K))
Tactic: simp only [AlgHom.map_adjoin_singleton, IsScalarTower.coe_toAlgHom', RingOfIntegers.map_mk,
      Algebra.map_top] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
n : ℕ
hn : NeZero n
⊢ IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)
have hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
Tactic: have hζ := zeta_spec n ℚ (CyclotomicField n ℚ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
n : ℕ
hn : NeZero n
hζ : IsPrimitiveRoot (M := CyclotomicField n ℚ) (zeta n ℚ (CyclotomicField n ℚ)) n
⊢ IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)
have refine_1 : ∀ {x : CyclotomicField n ℚ} (h : IsIntegral ℤ x),
  Membership.mem (γ := Subalgebra ℤ (CyclotomicField n ℚ)) (adjoin ℤ {b : CyclotomicField n ℚ | b ^ n = 1}) x
Tactic: refine ⟨IsFractionRing.injective _ _, fun {x} => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩