awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∀ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P →
          p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
              ⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ →
            Submodule.IsPrincipal P
x : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ P
hP :
  (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K)).IsPrime
hPN :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
                HP) :
            Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : IsPrime (under ℤ P) → _root_.Prime p
hlies : P.LiesOver (A := ℤ) (span {p})
hspan : Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have hple : p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P ≤
  ⌊(4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
Tactic: have hple : p.natAbs ^ (span {(p.natAbs : ℤ)}).inertiaDeg P ≤ ⌊(M K)⌋₊ := by
    refine le_floor ?_
    simpa only [hspan, ← cast_pow, ← absNorm_eq_pow_inertiaDeg P (hpprime (hP.under _))] using hPN
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∀ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P →
          p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
              ⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ →
            Submodule.IsPrincipal P
x : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ P
hP :
  (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K)).IsPrime
hPN :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
                HP) :
            Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : IsPrime (under ℤ P) → _root_.Prime p
hlies : P.LiesOver (A := ℤ) (span {p})
hspan : Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
hple :
  p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have hpabsprime : Nat.Prime p.natAbs
Tactic: have hpabsprime := Int.prime_iff_natAbs_prime.mp (hpprime (hP.under _))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∀ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P →
          p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
              ⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ →
            Submodule.IsPrincipal P
x : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ P
hP :
  (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K)).IsPrime
hPN :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
                HP) :
            Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : IsPrime (under ℤ P) → _root_.Prime p
hlies : P.LiesOver (A := ℤ) (span {p})
hspan : Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
hple :
  p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hpabsprime : Nat.Prime p.natAbs
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have refine_1 : p.natAbs ∈
  Finset.Icc 1
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
Tactic: refine h _ ?_ hpabsprime _ ⟨hP, ?_⟩ hple
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∀ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P →
          p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
              ⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ →
            Submodule.IsPrincipal P
x : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ P
hP :
  (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K)).IsPrime
hPN :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
                HP) :
            Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : IsPrime (under ℤ P) → _root_.Prime p
hlies : P.LiesOver (A := ℤ) (span {p})
hspan : Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
hple :
  p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hpabsprime : Nat.Prime p.natAbs
refine_1 :
  p.natAbs ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have refine_2 : (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K)).LiesOver
  (A := ℤ) (span {(↑p.natAbs : ℤ)})
Tactic: refine h _ ?_ hpabsprime _ ⟨hP, ?_⟩ hple
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∀ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P →
          p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
              ⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ →
            Submodule.IsPrincipal P
x : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ P
hP :
  (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K)).IsPrime
hPN :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
                HP) :
            Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : IsPrime (under ℤ P) → _root_.Prime p
hlies : P.LiesOver (A := ℤ) (span {p})
hspan : Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
hple :
  p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hpabsprime : Nat.Prime p.natAbs
⊢ p.natAbs ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
have refine_1 : 0 < inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P
Tactic: suffices 0 < (span {(p.natAbs : ℤ)}).inertiaDeg P by
      exact Finset.mem_Icc.mpr ⟨hpabsprime.one_le, le_trans (le_pow this) hple⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∀ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P →
          p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
              ⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ →
            Submodule.IsPrincipal P
x : ↥(Ideal (𝓞 K))⁰
P : Ideal (𝓞 K)
HP : Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ P
hP :
  (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K)).IsPrime
hPN :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
                HP) :
            Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
p : ℤ
hp : under ℤ P = ℤ ∙ p
hp0 : p ≠ 0
hpprime : IsPrime (under ℤ P) → _root_.Prime p
hlies : P.LiesOver (A := ℤ) (span {p})
hspan : Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
hple :
  p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hpabsprime : Nat.Prime p.natAbs
⊢ 0 < inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P
have this : IsMaximal (α := ℤ) (span {p})
Tactic: have := (isPrime_of_prime (prime_span_singleton_iff.mpr <|
      hpprime (hP.under _))).isMaximal <| by simp [((hpprime (hP.under _))).ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∃ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P ∧
          (⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
            Submodule.IsPrincipal P)
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)
have refine : ∀ (p : ℕ)
  (hpmem :
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊)
  (hp : Nat.Prime p) (P : Ideal (𝓞 K)),
  Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P →
    ∀
      (hple :
        p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
          ⌊(4 / π) ^ nrComplexPlaces K *
              ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊)
      (hP1 : P.IsPrime) (hP2 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})), Submodule.IsPrincipal P
Tactic: refine isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc
    (fun p hpmem hp P ⟨hP1, hP2⟩ hple ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∃ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P ∧
          (⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
            Submodule.IsPrincipal P)
p : ℕ
hpmem :
  p ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
h_1 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
⊢ Submodule.IsPrincipal P
have obtain : ∀ (Q : Ideal (𝓞 K))
  (H :
    ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
        p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q ∨
      Submodule.IsPrincipal Q)
  (hQ1 : Q.IsPrime) (hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})), Submodule.IsPrincipal P
Tactic: obtain ⟨Q, ⟨hQ1, hQ2⟩, H⟩ := h p hpmem hp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∃ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P ∧
          (⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
            Submodule.IsPrincipal P)
p : ℕ
hpmem :
  p ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
h_1 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
⊢ Submodule.IsPrincipal P
have this : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
Tactic: have := (isPrime_of_prime (prime_span_singleton_iff.mpr (prime_iff_prime_int.mp hp))).isMaximal
    (by simp [hp.ne_zero])
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∃ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P ∧
          (⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
            Submodule.IsPrincipal P)
p : ℕ
hpmem :
  p ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
h_1 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
⊢ Submodule.IsPrincipal P
have pos : ∀
  (h :
    ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P),
  Submodule.IsPrincipal P
Tactic: by_cases h : ⌊(M K)⌋₊ < p ^ ((span ({↑p} : Set ℤ)).inertiaDeg P)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h :
  ∀
    p ∈
      Finset.Icc 1
        ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊,
    Nat.Prime p →
      ∃ (P : Ideal (𝓞 K)),
        Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P ∧
          (⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
            Submodule.IsPrincipal P)
p : ℕ
hpmem :
  p ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
h_1 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) P
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (A := ℤ) (span {(↑p : ℤ)})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) Q ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
pos :
  ∀
    (h :
      ⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
        p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P),
    Submodule.IsPrincipal P
⊢ Submodule.IsPrincipal P
have neg : ∀
  (h :
    ¬⌊(4 / π) ^ nrComplexPlaces K *
            ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
        p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P),
  Submodule.IsPrincipal P
Tactic: by_cases h : ⌊(M K)⌋₊ < p ^ ((span ({↑p} : Set ℤ)).inertiaDeg P)