awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have hζ : IsPrimitiveRoot (zeta n ℚ K) n
Tactic: have hζ := zeta_spec n ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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)
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Tactic: have hζₘ := hζ.pow (NeZero.pos _) hn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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 := ℚ⟮ζₘ⟯
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have this₁ : IsCyclotomicExtension.{0, u_1} {m} ℚ ↥Fₘ
Tactic: have : IsCyclotomicExtension {m} ℚ Fₘ :=
    (isCyclotomicExtension_singleton_iff_eq_adjoin _ _ _ _ hζₘ).mpr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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ₘ
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have 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)
Tactic: obtain ⟨Pₘ, _, _⟩ := exists_maximal_ideal_liesOver_of_isIntegral 𝒑 (S := 𝓞 Fₘ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Tactic: have hζₚ := hζ.pow (NeZero.pos _) (mul_comm _ m ▸ hn)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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 := ℚ⟮ζₚ⟯
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have this₁ : IsCyclotomicExtension.{0, u_1} {p ^ (k + 1)} ℚ ↥Fₚ
Tactic: have : IsCyclotomicExtension {p ^ (k + 1)} ℚ Fₚ :=
    (isCyclotomicExtension_singleton_iff_eq_adjoin _ _ _ _ hζₚ).mpr rfl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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ₚ
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have 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)
Tactic: obtain ⟨Pₚ, hP₁, _⟩ := exists_maximal_ideal_liesOver_of_isIntegral 𝒑 (S := 𝓞 Fₚ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have this₁ : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
Tactic: replace this := Nat.eq_one_of_mul_eq_one_right this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have rw : orderOf (G := ZMod m) (↑p : ZMod m) = orderOf (G := ZMod m) (↑p : ZMod m) ∧ p ^ k * (p - 1) = 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ₚ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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 := ℤ) 𝒑
⊢ inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m) ∧
    ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
have suffices : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 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⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
have rw : (p ^ (k + 1)).Coprime m
Tactic: rw [finrank m, finrank (p ^ (k + 1)), finrank n, hn, mul_comm, Nat.totient_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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ₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
have h_main : 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])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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 := ℤ) 𝒑
h_main : Module.finrank.{0, u_1} ℚ ↥Fₘ * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
have rwa : ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K),
  Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
Tactic: rwa [← IsGalois.card_aut_eq_finrank, ← IsGalois.card_aut_eq_finrank,
    ← IsGalois.card_aut_eq_finrank,
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 Fₘ) Gal(Fₘ/ℚ),
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 Fₚ) Gal(Fₚ/ℚ),
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 K) Gal(K/ℚ),
    ← ncard_primesOver_mul_ncard_primesOver Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₘ) hp',
    ramificationIdxIn_eq_of_not_dvd p Fₘ hm, inertiaDegIn_eq_of_prime_pow p k Fₚ,
    ncard_primesOver_of_prime_pow p k Fₚ, one_mul, one_mul, mul_one, mul_assoc, mul_assoc,
    mul_right_inj' (IsDedekindDomain.primesOver_ncard_ne_zero 𝒑 _), ← mul_assoc,
    ← mul_rotate (𝒑.inertiaDegIn (𝓞 K)),
    ← inertiaDegIn_mul_inertiaDegIn 𝒑 Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₘ), mul_assoc, mul_assoc,
    mul_right_inj' (inertiaDegIn_ne_zero Gal(Fₘ/ℚ)), ← mul_rotate',
    ← ramificationIdxIn_mul_ramificationIdxIn' (p := 𝒑) Pₚ Gal(Fₚ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₚ),
    eq_comm, mul_assoc, mul_eq_left₀ (ramificationIdxIn_ne_zero Gal(Fₚ/ℚ) hp'), ← mul_assoc]
    at h_main
Cleared hypotheses: h_main
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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 := ℤ) 𝒑
h_main : Module.finrank.{0, u_1} ℚ ↥Fₘ * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K
rwa :
  ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K),
    Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
have rwa₁ : ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Nat.card.{u_1} Gal(↥Fₚ/ℚ) = Module.finrank ℚ K),
  Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
Tactic: rwa [← IsGalois.card_aut_eq_finrank, ← IsGalois.card_aut_eq_finrank,
    ← IsGalois.card_aut_eq_finrank,
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 Fₘ) Gal(Fₘ/ℚ),
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 Fₚ) Gal(Fₚ/ℚ),
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 K) Gal(K/ℚ),
    ← ncard_primesOver_mul_ncard_primesOver Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₘ) hp',
    ramificationIdxIn_eq_of_not_dvd p Fₘ hm, inertiaDegIn_eq_of_prime_pow p k Fₚ,
    ncard_primesOver_of_prime_pow p k Fₚ, one_mul, one_mul, mul_one, mul_assoc, mul_assoc,
    mul_right_inj' (IsDedekindDomain.primesOver_ncard_ne_zero 𝒑 _), ← mul_assoc,
    ← mul_rotate (𝒑.inertiaDegIn (𝓞 K)),
    ← inertiaDegIn_mul_inertiaDegIn 𝒑 Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₘ), mul_assoc, mul_assoc,
    mul_right_inj' (inertiaDegIn_ne_zero Gal(Fₘ/ℚ)), ← mul_rotate',
    ← ramificationIdxIn_mul_ramificationIdxIn' (p := 𝒑) Pₚ Gal(Fₚ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₚ),
    eq_comm, mul_assoc, mul_eq_left₀ (ramificationIdxIn_ne_zero Gal(Fₚ/ℚ) hp'), ← mul_assoc]
    at h_main
Cleared hypotheses: h_main
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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 := ℤ) 𝒑
h_main : Module.finrank.{0, u_1} ℚ ↥Fₘ * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K
rwa :
  ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Module.finrank.{0, u_1} ℚ ↥Fₚ = Module.finrank ℚ K),
    Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
rwa₁ :
  ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Nat.card.{u_1} Gal(↥Fₚ/ℚ) = Module.finrank ℚ K),
    Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
have rwa₂ : ∀ (h_main : Nat.card.{u_1} Gal(↥Fₘ/ℚ) * Nat.card.{u_1} Gal(↥Fₚ/ℚ) = Nat.card.{u_1} Gal(K/ℚ)),
  Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * Set.ncard (α := Ideal (𝓞 K)) (Pₘ.primesOver (𝓞 K)) = 1
Tactic: rwa [← IsGalois.card_aut_eq_finrank, ← IsGalois.card_aut_eq_finrank,
    ← IsGalois.card_aut_eq_finrank,
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 Fₘ) Gal(Fₘ/ℚ),
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 Fₚ) Gal(Fₚ/ℚ),
    ← ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn hp' (𝓞 K) Gal(K/ℚ),
    ← ncard_primesOver_mul_ncard_primesOver Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₘ) hp',
    ramificationIdxIn_eq_of_not_dvd p Fₘ hm, inertiaDegIn_eq_of_prime_pow p k Fₚ,
    ncard_primesOver_of_prime_pow p k Fₚ, one_mul, one_mul, mul_one, mul_assoc, mul_assoc,
    mul_right_inj' (IsDedekindDomain.primesOver_ncard_ne_zero 𝒑 _), ← mul_assoc,
    ← mul_rotate (𝒑.inertiaDegIn (𝓞 K)),
    ← inertiaDegIn_mul_inertiaDegIn 𝒑 Pₘ Gal(Fₘ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₘ), mul_assoc, mul_assoc,
    mul_right_inj' (inertiaDegIn_ne_zero Gal(Fₘ/ℚ)), ← mul_rotate',
    ← ramificationIdxIn_mul_ramificationIdxIn' (p := 𝒑) Pₚ Gal(Fₚ/ℚ) (𝓞 K) Gal(K/ℚ) Gal(K/Fₚ),
    eq_comm, mul_assoc, mul_eq_left₀ (ramificationIdxIn_ne_zero Gal(Fₚ/ℚ) hp'), ← mul_assoc]
    at h_main
Cleared hypotheses: h_main
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have this : IsGalois ℚ K
Tactic: have : IsGalois ℚ K := isGalois {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have rw : inertiaDegIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = orderOf (G := ZMod m) (↑p : ZMod m)
Tactic: rw [← inertiaDegIn_eq_inertiaDeg 𝒑 P Gal(K/ℚ), inertiaDegIn_eq n K hn hm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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)
⊢ inertiaDeg (R := ℤ) 𝒑 P = orderOf (G := ZMod m) (↑p : ZMod m)
have rw₁ : orderOf (G := ZMod m) (↑p : ZMod m) = orderOf (G := ZMod m) (↑p : ZMod m)
Tactic: rw [← inertiaDegIn_eq_inertiaDeg 𝒑 P Gal(K/ℚ), inertiaDegIn_eq n K hn hm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (hypothesis)
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
⊢ ramificationIdx (R := ℤ) 𝒑 P = p ^ k * (p - 1)
have this : IsGalois ℚ K
Tactic: have : IsGalois ℚ K := isGalois {n} ℚ K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal (goal)
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
⊢ ramificationIdx (R := ℤ) 𝒑 P = p ^ k * (p - 1)
have rw : ramificationIdxIn.{0, u_1} (A := ℤ) 𝒑 (𝓞 K) = p ^ k * (p - 1)
Tactic: rw [← ramificationIdxIn_eq_ramificationIdx 𝒑 P Gal(K/ℚ), ramificationIdxIn_eq n K hn hm]