awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
⊢ IsMaximal (α := ℤ) (span {p})

Tactic:
have := (isPrime_of_prime (prime_span_singleton_iff.mpr <|
      hpprime (hP.under _))).isMaximal <| by simp [((hpprime (hP.under _))).ne_zero]
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
this : IsMaximal (α := ℤ) (span {p})
⊢ 0 < inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P

Tactic:
hspan ▸ inertiaDeg_pos ..

Premises used: Eq.rec, Ideal.inertiaDeg_pos, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
this : IsMaximal (α := ℤ) (span {p})
⊢ 0 < inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P

Tactic:
exact hspan ▸ inertiaDeg_pos ..
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
⊢ (↑(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:
hspan ▸ hlies

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
⊢ (↑(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:
exact hspan ▸ hlies
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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)

Tactic:
isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc
    (fun p hpmem hp P ⟨hP1, hP2⟩ hple ↦ ?_)

Premises used: RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc, _private.0.RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc.match_1, Submodule.IsPrincipal
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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)
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
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)

Tactic:
refine isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc
    (fun p hpmem hp P ⟨hP1, hP2⟩ hple ↦ ?_)

Premises used: RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_pow_le_of_mem_primesOver_of_mem_Icc
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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 : ℤ)})
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
⊢ Submodule.IsPrincipal P

Tactic:
obtain ⟨Q, ⟨hQ1, hQ2⟩, H⟩ := h p hpmem hp
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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 : ℤ)})
⊢ Ne (α := Ideal ℤ) (span {(↑p : ℤ)}) ⊥

Tactic:
simp [hp.ne_zero]

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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 : ℤ)})
⊢ 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])
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
neg :
  ∀
    (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

Tactic:
by_cases h : ⌊(M K)⌋₊ < p ^ ((span ({↑p} : Set ℤ)).inertiaDeg P)

Premises used: Int.cast, Real.pi, HMul.hMul, abs, Rat, Ideal.inertiaDeg, HDiv.hDiv, Nat.cast, HPow.hPow, Nat.factorial, Real.sqrt, NumberField.discr, Ideal.span, NumberField.InfinitePlace.nrComplexPlaces, Singleton.singleton, OfNat.ofNat, Module.finrank
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : IsGalois ℚ K
h_1 :
  ∀
    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_2 : 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 : ℤ)})
h :
  ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
    p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P
linarith :
  -1 +
        (HPow.hPow (α := ℤ) (↑p : ℤ) (inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P) -
          (↑⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ :
            ℤ)) +
      (HAdd.hAdd (α := ℤ)
          (↑⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ :
            ℤ)
          1 -
        HPow.hPow (α := ℤ) (↑p : ℤ) (inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P)) =
    0
⊢ Submodule.IsPrincipal P

Tactic:
linarith