awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
    Submodule.IsPrincipal Q

Tactic:
rw [inertiaDeg_eq_of_isGaloisGroup _ Q P (K ≃ₐ[ℚ] K)] at H

Premises used: Rat, Ideal.inertiaDeg_eq_of_isGaloisGroup, AlgEquiv
-- 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
H₁ :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
    Submodule.IsPrincipal Q
⊢ Q.IsPrime

Tactic:
rw [inertiaDeg_eq_of_isGaloisGroup _ Q P (K ≃ₐ[ℚ] K)] at H

Premises used: Rat, Ideal.inertiaDeg_eq_of_isGaloisGroup, AlgEquiv
-- 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
H₁ :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
    Submodule.IsPrincipal Q
hQ1₁ : Q.IsPrime
⊢ Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})

Tactic:
rw [inertiaDeg_eq_of_isGaloisGroup _ Q P (K ≃ₐ[ℚ] K)] at H

Premises used: Rat, Ideal.inertiaDeg_eq_of_isGaloisGroup, AlgEquiv
-- 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
H₁ :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
    Submodule.IsPrincipal Q
hQ1₁ : Q.IsPrime
hQ2₁ : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
⊢ IsMaximal (α := ℤ) (span {(↑p : ℤ)})

Tactic:
rw [inertiaDeg_eq_of_isGaloisGroup _ Q P (K ≃ₐ[ℚ] K)] at H

Premises used: Rat, Ideal.inertiaDeg_eq_of_isGaloisGroup, AlgEquiv
-- 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
H₁ :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P ∨
    Submodule.IsPrincipal Q
hQ1₁ : Q.IsPrime
hQ2₁ : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this₁ : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
⊢ ¬⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) P

Tactic:
rw [inertiaDeg_eq_of_isGaloisGroup _ Q P (K ≃ₐ[ℚ] K)] at H

Premises used: Rat, Ideal.inertiaDeg_eq_of_isGaloisGroup, AlgEquiv
-- 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 : ℤ)}) P ∨
    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
neg :
  ∀ (σ : Gal(K/ℚ)),
    Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) (σ • Q) →
      ∀
        (hple :
          p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q) ≤
            ⌊(4 / π) ^ nrComplexPlaces K *
                ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊)
        (hP1 : (σ • Q).IsPrime) (hP2 : (σ • Q).LiesOver (A := ℤ) (span {(↑p : ℤ)}))
        (H :
          ⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q) ∨
            Submodule.IsPrincipal Q)
        (h :
          ¬⌊(4 / π) ^ nrComplexPlaces K *
                  ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
                    √|(↑(discr K) : ℝ)|)⌋₊ <
              p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q)),
        Submodule.IsPrincipal (σ • Q)
⊢ Submodule.IsPrincipal P

Tactic:
obtain ⟨σ, rfl⟩ := exists_smul_eq_of_isGaloisGroup (span ({↑p} : Set ℤ)) Q P (K ≃ₐ[ℚ] K)

Premises used: Ideal.exists_smul_eq_of_isGaloisGroup, Rat, AlgEquiv, Ideal.span, Singleton.singleton, rfl
-- 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
Q : Ideal (𝓞 K)
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
σ : Gal(K/ℚ)
h_2 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) (σ • Q)
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q) ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : (σ • Q).IsPrime
hP2 : (σ • Q).LiesOver (A := ℤ) (span {(↑p : ℤ)})
H :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q) ∨
    Submodule.IsPrincipal Q
h :
  ¬⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q)
⊢ Submodule.IsPrincipal (σ • Q)

Tactic:
(H.resolve_left h).map_ringHom (MulSemiringAction.toRingHom (K ≃ₐ[ℚ] K) (𝓞 K) σ)

Premises used: Submodule.IsPrincipal.map_ringHom, Rat, MulSemiringAction.toRingHom, Or.resolve_left, AlgEquiv, NumberField.RingOfIntegers
-- 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
Q : Ideal (𝓞 K)
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (A := ℤ) (span {(↑p : ℤ)})
this : IsMaximal (α := ℤ) (span {(↑p : ℤ)})
σ : Gal(K/ℚ)
h_2 : Membership.mem (γ := Set (Ideal (𝓞 K))) (primesOver (A := ℤ) (span {(↑p : ℤ)}) (𝓞 K)) (σ • Q)
hple :
  p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q) ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
hP1 : (σ • Q).IsPrime
hP2 : (σ • Q).LiesOver (A := ℤ) (span {(↑p : ℤ)})
H :
  ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q) ∨
    Submodule.IsPrincipal Q
h :
  ¬⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊ <
      p ^ inertiaDeg (R := ℤ) (span {(↑p : ℤ)}) (σ • Q)
⊢ Submodule.IsPrincipal (σ • Q)

Tactic:
exact (H.resolve_left h).map_ringHom (MulSemiringAction.toRingHom (K ≃ₐ[ℚ] K) (𝓞 K) σ)

Premises used: Submodule.IsPrincipal.map_ringHom, Rat, MulSemiringAction.toRingHom, Or.resolve_left, AlgEquiv, NumberField.RingOfIntegers
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (↑|discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ)))
      2
⊢ 0 < finrank ℚ K

Tactic:
have : 0 < finrank ℚ K := finrank_pos
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (↑|discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ)))
      2
this : 0 < finrank ℚ K
⊢ LE.le (α := ℝ) 0 (↑|discr K| : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (↑|discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ)))
      2
this : 0 < finrank ℚ K
⊢ 0 ≤ 2 * (π / 4) ^ nrComplexPlaces K * (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ))

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  √(↑|discr K| : ℝ) <
    2 * ((π / 4) ^ nrComplexPlaces K * (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ)))
this : 0 < finrank ℚ K
⊢ 0 < (π / 4) ^ nrComplexPlaces K * (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ))

Tactic:
positivity
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (↑|discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ)))
      2
this : 0 < finrank ℚ K
⊢ (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) <
    2

Tactic:
rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff₀' (by positivity),
    mul_inv, ← inv_pow, inv_div, inv_div, mul_assoc, Int.cast_abs] at h

Premises used: Int.cast_abs, mul_inv, mul_assoc, inv_pow, inv_mul_lt_iff₀', inv_div, Real.sqrt_lt
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (↑|discr K| : ℝ) <
    HPow.hPow (β := ℕ)
      (2 * (π / 4) ^ nrComplexPlaces K *
        (HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) / (↑(finrank ℚ K)! : ℝ)))
      2
this : 0 < finrank ℚ K
h₁ :
  (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) <
    2
⊢ 0 < finrank ℚ K

Tactic:
rw [← Real.sqrt_lt (by positivity) (by positivity), mul_assoc, ← inv_mul_lt_iff₀' (by positivity),
    mul_inv, ← inv_pow, inv_div, inv_div, mul_assoc, Int.cast_abs] at h

Premises used: Int.cast_abs, mul_inv, mul_assoc, inv_pow, inv_mul_lt_iff₀', inv_div, Real.sqrt_lt
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) <
    2
this : 0 < finrank ℚ K
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)

Tactic:
isPrincipalIdealRing_of_isPrincipal_of_norm_le (fun I hI ↦ ?_)

Premises used: RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|) <
    2
this : 0 < finrank ℚ K
refine :
  ∀ (I : ↥(Ideal (𝓞 K))⁰)
    (hI :
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)),
    Submodule.IsPrincipal (↑I : Ideal (𝓞 K))
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)

Tactic:
refine isPrincipalIdealRing_of_isPrincipal_of_norm_le (fun I hI ↦ ?_)

Premises used: RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le