awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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
⊢ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (isPrincipalSubmonoid (𝓞 K))
    (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J ⋯) : Ideal (𝓞 K))
have neg : (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ)
        (↑(Subtype.mk (p := Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰) J sorry) : Ideal (𝓞 K))) :
    ℝ) ≤
  (4 / π) ^ nrComplexPlaces K *
    ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
Tactic: refine h (((mem_normalizedFactors_iff (nonZeroDivisors.coe_ne_zero I)).mp hJ).1) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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)
have 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))
Tactic: refine isPrincipalIdealRing_of_isPrincipal_of_norm_le_of_isPrime <|
    fun ⟨P, HP⟩ hP hPN ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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) : ℝ)|)
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have 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))
Tactic: obtain ⟨p, hp⟩ := IsPrincipalIdealRing.principal <| under ℤ P
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
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
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have hp0 : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
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
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have hpprime : IsPrime (α := ℤ) (span {p}) → _root_.Prime p
Tactic: have hpprime := (span_singleton_prime hp0).mp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
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
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have hpprime₁ : IsPrime (under ℤ P) → _root_.Prime p
Tactic: simp only [← submodule_span_eq, ← hp] at hpprime
Cleared hypotheses: hpprime
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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})
have inl : ∀ (h : |p| = p), P.LiesOver (A := ℤ) (span {p})
Tactic: rcases abs_choice p with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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})
⊢ P.LiesOver (A := ℤ) (span {p})
have inr : ∀ (h : |p| = -p), P.LiesOver (A := ℤ) (span {p})
Tactic: rcases abs_choice p with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
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
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have hlies : 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
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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})
have inl : ∀ (h : |p| = p), Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
Tactic: rcases abs_choice p with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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})
⊢ Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
have inr : ∀ (h : |p| = -p), Eq (α := Ideal ℤ) (span {(↑p.natAbs : ℤ)}) (span {p})
Tactic: rcases abs_choice p with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
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})
⊢ Submodule.IsPrincipal
    (↑(Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) P HP) :
      Ideal (𝓞 K))
have hspan : 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]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
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) : ℝ)|)⌋₊
have refine : (↑(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 ?_