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 :
  ∀ ⦃I : ↥(Ideal (𝓞 K))⁰⦄,
    (↑I : Ideal (𝓞 K)).IsPrime →
      (↑((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))
I : ↥(Ideal (𝓞 K))⁰
hI :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
J : Ideal (𝓞 K)
hJ : J ∈ UniqueFactorizationMonoid.normalizedFactors (↑I : Ideal (𝓞 K))
hJ0 : ¬J = 0
⊢ (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
          (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J ⋯) : Ideal (𝓞 K))) :
      ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)

Tactic:
exact (cast_le.mpr <| le_of_dvd (absNorm_pos_of_nonZeroDivisors I) <|
    absNorm_dvd_absNorm_of_le <| le_of_dvd <|
      UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hJ).trans hI

Premises used: Iff.mpr, UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors, Ideal.le_of_dvd, Ideal.absNorm_dvd_absNorm_of_le, Ideal.absNorm_pos_of_nonZeroDivisors, Nat.cast_le, LE.le.trans, Nat.le_of_dvd
-- 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
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)

Tactic:
isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime <|
    fun ⟨P, HP⟩ hP hPN ↦ ?_

Premises used: RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime
-- 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
refine :
  ∀ (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) : ℝ)|)),
    Submodule.IsPrincipal
      (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
            HP) :
        Ideal (𝓞 K))
⊢ IsPrincipalIdealRing.{u_1} (𝓞 K)

Tactic:
refine isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime <|
    fun ⟨P, HP⟩ hP hPN ↦ ?_

Premises used: RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime
-- 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) : ℝ)|)
obtain :
  ∀ (p : ℤ) (hp : under ℤ P = ℤ ∙ p),
    Submodule.IsPrincipal
      (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
            HP) :
        Ideal (𝓞 K))
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))

Tactic:
obtain ⟨p, hp⟩ := IsPrincipalIdealRing.principal <| under ℤ P

Premises used: Int, IsPrincipalIdealRing.principal, Ideal.under
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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 →
          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
h : p = 0
⊢ Eq (α := Ideal ℤ)
    (Ideal.comap (F := ℤ →+* 𝓞 K) (algebraMap ℤ (𝓞 K))
      (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P
            HP) :
        Ideal (𝓞 K)))
    ⊥

Tactic:
simpa only [hp, submodule_span_eq, span_singleton_eq_bot]

Premises used: Ideal.span_singleton_eq_bot, Ideal.submodule_span_eq
-- 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
⊢ p ≠ 0

Tactic:
have hp0 : p ≠ 0 := fun h ↦ nonZeroDivisors.coe_ne_zero ⟨P, HP⟩ <|
    eq_bot_of_comap_eq_bot (R := ℤ) <| by simpa only [hp, submodule_span_eq, span_singleton_eq_bot]
-- 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
⊢ IsPrime (α := ℤ) (span {p}) → _root_.Prime p

Tactic:
have hpprime := (span_singleton_prime hp0).mp
-- 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 (α := ℤ) (span {p}) → _root_.Prime p
⊢ IsPrime (under ℤ P) → _root_.Prime p

Tactic:
simp only [← submodule_span_eq, ← hp] at hpprime

Premises used: Ideal.submodule_span_eq
-- 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
inl : ∀ (h : |p| = p), P.LiesOver (A := ℤ) (span {p})
inr : ∀ (h : |p| = -p), P.LiesOver (A := ℤ) (span {p})
⊢ P.LiesOver (A := ℤ) (span {p})

Tactic:
rcases abs_choice p with h | h

Premises used: abs_choice
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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 →
          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
h : |p| = p
⊢ P.LiesOver (A := ℤ) (span {p})

Tactic:
simpa [h, span_singleton_neg p, ← submodule_span_eq, ← hp] using over_under P

Premises used: Ideal.submodule_span_eq, Ideal.over_under, Ideal.span_singleton_neg
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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 →
          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
h : |p| = -p
⊢ P.LiesOver (A := ℤ) (span {p})

Tactic:
simpa [h, span_singleton_neg p, ← submodule_span_eq, ← hp] using over_under P

Premises used: Ideal.submodule_span_eq, Ideal.over_under, Ideal.span_singleton_neg
-- 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
⊢ P.LiesOver (A := ℤ) (span {p})

Tactic:
have hlies : P.LiesOver (span {p}) := by
    rcases abs_choice p with h | h <;>
    simpa [h, span_singleton_neg p, ← submodule_span_eq, ← hp] using over_under P
-- 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})
inl : ∀ (h : |p| = p), Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
inr : ∀ (h : |p| = -p), Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
⊢ Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})

Tactic:
rcases abs_choice p with h | h

Premises used: abs_choice
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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 →
          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})
h : |p| = p
⊢ Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField 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 →
          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})
h : |p| = -p
⊢ Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})

Tactic:
simp [h]