Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsGalois ℚ K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∃ P ∈ (span {↑p}).primesOver (𝓞 K),
        ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
            p ^ P.inertiaDeg ℤ ∨
          Submodule.IsPrincipal P
p : ℕ
hpmem :
  p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
x✝ : P ∈ (span {↑p}).primesOver (𝓞 K)
hple :
  p ^ P.inertiaDeg ℤ ≤ ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (span {↑p})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
      p ^ Q.inertiaDeg ℤ ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (span {↑p})
this : (span {↑p}).IsMaximal
⊢ Submodule.IsPrincipal P

Tactic:
by_cases h : ⌊(M K)⌋₊ < p ^ P.inertiaDeg ℤ

Goal state after:
case pos
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsGalois ℚ K
h✝ :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∃ P ∈ (span {↑p}).primesOver (𝓞 K),
        ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
            p ^ P.inertiaDeg ℤ ∨
          Submodule.IsPrincipal P
p : ℕ
hpmem :
  p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
x✝ : P ∈ (span {↑p}).primesOver (𝓞 K)
hple :
  p ^ P.inertiaDeg ℤ ≤ ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (span {↑p})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
      p ^ Q.inertiaDeg ℤ ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (span {↑p})
this : (span {↑p}).IsMaximal
h :
  ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ < p ^ P.inertiaDeg ℤ
⊢ Submodule.IsPrincipal P

case neg
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsGalois ℚ K
h✝ :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∃ P ∈ (span {↑p}).primesOver (𝓞 K),
        ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
            p ^ P.inertiaDeg ℤ ∨
          Submodule.IsPrincipal P
p : ℕ
hpmem :
  p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
x✝ : P ∈ (span {↑p}).primesOver (𝓞 K)
hple :
  p ^ P.inertiaDeg ℤ ≤ ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (span {↑p})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
      p ^ Q.inertiaDeg ℤ ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (span {↑p})
this : (span {↑p}).IsMaximal
h :
  ¬⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
      p ^ P.inertiaDeg ℤ
⊢ Submodule.IsPrincipal P