awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
this : IsGalois ℚ K
P : Ideal (𝓞 K)
left : P.IsPrime
right : P.LiesOver (A := ℤ) 𝒑
rw : ramificationIdx (R := ℤ) 𝒑 P = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = 1

Tactic:
rw [ramificationIdxIn_eq_ramificationIdx 𝒑 P Gal(K/ℚ), ramificationIdx_eq_of_not_dvd p K P hm]

Premises used: IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
⊢ IsAbelianGalois ℚ K

Tactic:
have : IsAbelianGalois ℚ K := IsCyclotomicExtension.isAbelianGalois {n} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this : IsAbelianGalois ℚ K
h : m = 0
⊢ False

Tactic:
simp [h] at hm
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this : IsAbelianGalois ℚ K
⊢ NeZero m

Tactic:
have : NeZero m := ⟨fun h ↦ by simp [h] at hm⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this : NeZero m
⊢ NeZero n

Tactic:
have : NeZero n := ⟨hn ▸ NeZero.ne (p ^ (k + 1) * m)⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this : NeZero n
⊢ Ne (α := Ideal ℤ) 𝒑 ⊥

Tactic:
simpa using hp.out.ne_zero

Premises used: Nat.Prime.ne_zero, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this : NeZero n
⊢ Ne (α := Ideal ℤ) 𝒑 ⊥

Tactic:
have hp' : 𝒑 ≠ ⊥ := by simpa using hp.out.ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
⊢ IsPrimitiveRoot (zeta n ℚ K) n

Tactic:
have hζ := zeta_spec n ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
⊢ IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m

Tactic:
have hζₘ := hζ.pow (NeZero.pos _) hn
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
⊢ IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ

Tactic:
have : IsCyclotomicExtension {m} ℚ Fₘ :=
    (isCyclotomicExtension_singleton_iff_eq_adjoin _ _ _ _ hζₘ).mpr rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
obtain :
  ∀ (Pₘ : Ideal (𝓞 ↥Fₘ)),
    Pₘ.IsMaximal →
      Pₘ.LiesOver (A := ℤ) 𝒑 →
        inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
          ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)

Tactic:
obtain ⟨Pₘ, _, _⟩ := exists_maximal_ideal_liesOver_of_isIntegral 𝒑 (S := 𝓞 Fₘ)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
⊢ IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))

Tactic:
have hζₚ := hζ.pow (NeZero.pos _) (mul_comm _ m ▸ hn)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
⊢ IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ

Tactic:
have : IsCyclotomicExtension {p ^ (k + 1)} ℚ Fₚ :=
    (isCyclotomicExtension_singleton_iff_eq_adjoin _ _ _ _ hζₚ).mpr rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
obtain :
  ∀ (Pₚ : Ideal (𝓞 ↥Fₚ)) (hP₁ : Pₚ.IsMaximal),
    Pₚ.LiesOver (A := ℤ) 𝒑 →
      inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
        ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)

Tactic:
obtain ⟨Pₚ, hP₁, _⟩ := exists_maximal_ideal_liesOver_of_isIntegral 𝒑 (S := 𝓞 Fₚ)
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this_5 : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1

Tactic:
replace this := Nat.eq_one_of_mul_eq_one_right this
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this_5 : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
rw : orderOf (G := ZMod m) (↑p : ZMod m) = orderOf (G := ZMod m) (↑p : ZMod m) ∧ p ^ k * (p - 1) = p ^ k * (p - 1)
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)

Tactic:
rw [← inertiaDegIn_mul_inertiaDegIn 𝒑 Pₘ Gal(Fₘ/ℚ) _ Gal(K/ℚ) Gal(K/Fₘ),
      ← ramificationIdxIn_mul_ramificationIdxIn' Pₚ Gal(Fₚ/ℚ) _ Gal(K/ℚ) Gal(K/Fₚ),
      Nat.eq_one_of_mul_eq_one_left this, Nat.eq_one_of_mul_eq_one_right this, mul_one, mul_one,
      inertiaDegIn_eq_of_not_dvd p _ hm, ramificationIdxIn_eq_of_prime_pow p k Fₚ]

Premises used: Rat, Membership.mem, Subtype, Nat.eq_one_of_mul_eq_one_right, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, Ideal.ramificationIdxIn_mul_ramificationIdxIn', Nat.eq_one_of_mul_eq_one_left, AlgEquiv, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, mul_one
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this_5 : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
⊢ orderOf (G := ZMod m) (↑p : ZMod m) = orderOf (G := ZMod m) (↑p : ZMod m) ∧ p ^ k * (p - 1) = p ^ k * (p - 1)

Tactic:
⟨rfl, rfl⟩

Premises used: And.intro, rfl
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this_5 : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
⊢ orderOf (G := ZMod m) (↑p : ZMod m) = orderOf (G := ZMod m) (↑p : ZMod m) ∧ p ^ k * (p - 1) = p ^ k * (p - 1)

Tactic:
exact ⟨rfl, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
suffices : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)

Tactic:
suffices Pₚ.ramificationIdxIn (𝓞 K) *
      Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1 by
    replace this := Nat.eq_one_of_mul_eq_one_right this
    rw [← inertiaDegIn_mul_inertiaDegIn 𝒑 Pₘ Gal(Fₘ/ℚ) _ Gal(K/ℚ) Gal(K/Fₘ),
      ← ramificationIdxIn_mul_ramificationIdxIn' Pₚ Gal(Fₚ/ℚ) _ Gal(K/ℚ) Gal(K/Fₚ),
      Nat.eq_one_of_mul_eq_one_left this, Nat.eq_one_of_mul_eq_one_right this, mul_one, mul_one,
      inertiaDegIn_eq_of_not_dvd p _ hm, ramificationIdxIn_eq_of_prime_pow p k Fₚ]
    exact ⟨rfl, rfl⟩
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
rw : (p ^ (k + 1)).Coprime m
⊢ Module.finrank.{0, u_1} ℚ ↥Fₘ * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K

Tactic:
rw [finrank m, finrank (p ^ (k + 1)), finrank n, hn, mul_comm, Nat.totient_mul]

Premises used: Nat.totient_mul, HPow.hPow, HAdd.hAdd, mul_comm, IsCyclotomicExtension.Rat.finrank, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
rwa rwa₁ rwa₂ rwa₃ : ¬p ∣ m
⊢ p.Coprime m

Tactic:
rwa [hp.out.coprime_iff_not_dvd]

Premises used: Nat.Prime.coprime_iff_not_dvd, Fact.out
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
⊢ (p ^ (k + 1)).Coprime m

Tactic:
exact Nat.Coprime.pow_left (k + 1) (by rwa [hp.out.coprime_iff_not_dvd])

Premises used: Nat.Coprime.pow_left, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this_1 : IsAbelianGalois ℚ K
this_2 : NeZero m
this_3 : NeZero n
hp' : Ne (α := Ideal ℤ) 𝒑 ⊥
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this_4 : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left : Pₘ.IsMaximal
right : Pₘ.LiesOver (A := ℤ) 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right_1 : Pₚ.LiesOver (A := ℤ) 𝒑
⊢ Module.finrank.{0, u_1} ℚ ↥Fₘ * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K

Tactic:
have h_main : Module.finrank ℚ Fₘ * Module.finrank ℚ Fₚ = Module.finrank ℚ K := by
    rw [finrank m, finrank (p ^ (k + 1)), finrank n, hn, mul_comm, Nat.totient_mul]
    exact Nat.Coprime.pow_left (k + 1) (by rwa [hp.out.coprime_iff_not_dvd])
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m)

Tactic:
(inertiaDegIn_ramificationIdxIn_aux n K hn hm).1

Premises used: _private.0.IsCyclotomicExtension.Rat.inertiaDegIn_ramificationIdxIn_aux, And.left
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
⊢ ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)

Tactic:
(inertiaDegIn_ramificationIdxIn_aux n K hn hm).2

Premises used: _private.0.IsCyclotomicExtension.Rat.inertiaDegIn_ramificationIdxIn_aux, And.right
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
⊢ IsGalois ℚ K

Tactic:
have : IsGalois ℚ K := isGalois {n} ℚ K
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this : IsGalois ℚ K
rw : inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m)
rw₁ rw₂ : orderOf (G := ZMod m) (↑p : ZMod m) = orderOf (G := ZMod m) (↑p : ZMod m)
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)

Tactic:
rw [← inertiaDegIn_eq_inertiaDeg 𝒑 P Gal(K/ℚ), inertiaDegIn_eq n K hn hm]

Premises used: IsCyclotomicExtension.Rat.inertiaDegIn_eq
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
Goal:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver (A := ℤ) 𝒑
inst_2 : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this : IsGalois ℚ K
rw : ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
rw₁ rw₂ : p ^ k * (p - 1) = p ^ k * (p - 1)
⊢ ramificationIdx (R := ℤ) 𝒑 P = p ^ k * (p - 1)

Tactic:
rw [← ramificationIdxIn_eq_ramificationIdx 𝒑 P Gal(K/ℚ), ramificationIdxIn_eq n K hn hm]

Premises used: IsCyclotomicExtension.Rat.ramificationIdxIn_eq
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h :
  (↑|NumberField.discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(Module.finrank ℚ K) : ℝ) (Module.finrank ℚ K) / (↑(Module.finrank ℚ K)! : ℝ)))
      2
⊢ IsPrincipalIdealRing.{u} (𝓞 K)

Tactic:
apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt

Premises used: RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
⊢ LT.lt (α := ℕ) 0 3

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Goal:
K : Type u
inst : Field K
inst_1 : NumberField K
inst_2 : IsCyclotomicExtension {3} ℚ K
h :
  (↑|HPow.hPow (α := ℤ) (-1) (HSub.hSub (α := ℕ) 3 1 / 2) * HPow.hPow (α := ℤ) (↑3 : ℤ) (HSub.hSub (α := ℕ) 3 2)| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ (HSub.hSub (α := ℕ) 3 1 / 2) *
        (HPow.hPow (α := ℝ) (↑(HSub.hSub (α := ℕ) 3 1) : ℝ) (HSub.hSub (α := ℕ) 3 1) /
          (↑(HSub.hSub (α := ℕ) 3 1)! : ℝ)))
      2
⊢ (↑|NumberField.discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(Module.finrank ℚ K) : ℝ) (Module.finrank ℚ K) / (↑(Module.finrank ℚ K)! : ℝ)))
      2

Tactic:
rw [discr_prime 3 K, IsCyclotomicExtension.finrank (n := 3) K
    (irreducible_rat (by simp)), nrComplexPlaces_eq_totient_div_two 3, totient_prime
      Nat.prime_three]

Premises used: IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two, Nat.totient_prime, IsCyclotomicExtension.finrank, Nat.prime_three, Polynomial.cyclotomic.irreducible_rat, OfNat.ofNat, IsCyclotomicExtension.Rat.discr_prime