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})
⊢ Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})

Tactic:
have hspan : span {↑p.natAbs} = span {p} := by
    rcases abs_choice p with h | h <;> simp [h]
-- 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})
⊢ p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊

Tactic:
le_floor ?_

Premises used: Nat.le_floor
-- 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})
refine :
  (↑(p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
⊢ p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P ≤
    ⌊(4 / π) ^ nrComplexPlaces K *
        ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊

Tactic:
refine le_floor ?_

Premises used: Nat.le_floor
-- 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})
⊢ (↑(p.natAbs ^ inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P) : ℝ) ≤
    (4 / π) ^ nrComplexPlaces K *
      ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)

Tactic:
simpa only [hspan, ← cast_pow, ← absNorm_eq_pow_inertiaDeg P (hpprime (hP.under _))] using hPN

Premises used: Ideal.absNorm_eq_pow_inertiaDeg, Nat.cast_pow, Ideal.IsPrime.under
-- 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})
⊢ 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
-- 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) : ℝ)|)⌋₊
⊢ Nat.Prime p.natAbs

Tactic:
have hpabsprime := Int.prime_iff_natAbs_prime.mp (hpprime (hP.under _))
-- 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
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))

Tactic:
h _ ?_ hpabsprime _ ⟨hP, ?_⟩ hple

Premises used: And.intro
-- 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
refine_1 :
  p.natAbs ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊
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 : ℤ)})
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))

Tactic:
refine h _ ?_ hpabsprime _ ⟨hP, ?_⟩ hple

Premises used: And.intro
-- 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 : 0 < inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P
⊢ p.natAbs ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊

Tactic:
Finset.mem_Icc.mpr ⟨hpabsprime.one_le, le_trans (le_pow this) hple⟩

Premises used: Iff.mpr, Finset.mem_Icc, Nat.le_pow, Nat.Prime.one_le, And.intro, le_trans
-- 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 : 0 < inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P
⊢ p.natAbs ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊

Tactic:
exact Finset.mem_Icc.mpr ⟨hpabsprime.one_le, le_trans (le_pow this) hple⟩

Premises used: Iff.mpr, Finset.mem_Icc, Nat.le_pow, Nat.Prime.one_le, And.intro, le_trans
-- 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
refine_1 : 0 < inertiaDeg (R := ℤ) (span {(↑p.natAbs : ℤ)}) P
⊢ p.natAbs ∈
    Finset.Icc 1
      ⌊(4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)⌋₊

Tactic:
suffices 0 < (span {(p.natAbs : ℤ)}).inertiaDeg P by
      exact Finset.mem_Icc.mpr ⟨hpabsprime.one_le, le_trans (le_pow this) hple⟩
-- 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
⊢ Ne (α := Ideal ℤ) (span {p}) ⊥

Tactic:
simp [((hpprime (hP.under _))).ne_zero]

Premises used: Prime.ne_zero, Ideal.IsPrime.under