awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
⊢ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
have refine_1 : ∀ x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A,
  ∀ (a : mixedSpace K) (ha₁ : a ∈ plusPart A) (ha₂ : normAtComplexPlaces a = normAtComplexPlaces x), x ∈ A
Tactic: refine subset_antisymm (fun x ⟨a, ha₁, ha₂⟩ ↦ ⟨?_, fun w ↦ ?_⟩) (Set.subset_preimage_image _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
refine_1 :
  ∀ x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A,
    ∀ (a : mixedSpace K) (ha₁ : a ∈ plusPart A) (ha₂ : normAtComplexPlaces a = normAtComplexPlaces x), x ∈ A
⊢ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
have refine_2 : ∀ x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A,
  ∀ (a : mixedSpace K) (ha₁ : a ∈ plusPart A) (ha₂ : normAtComplexPlaces a = normAtComplexPlaces x)
    (w : { w : InfinitePlace K // w.IsReal }), 0 < x.1 w
Tactic: refine subset_antisymm (fun x ⟨a, ha₁, ha₂⟩ ↦ ⟨?_, fun w ↦ ?_⟩) (Set.subset_preimage_image _ _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ x ∈ A
have refine_1 : normAtAllPlaces a ∈ normAtAllPlaces '' A
Tactic: rw [← hA, Set.mem_preimage, ← normAtAllPlaces_eq_of_normAtComplexPlaces_eq ha₂]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (hypothesis)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w : InfinitePlace K // w.IsReal }
⊢ 0 < x.1 w
have this : normAtComplexPlaces a (↑w : InfinitePlace K) = normAtComplexPlaces x (↑w : InfinitePlace K)
Tactic: have := funext_iff.mp ha₂ w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (hypothesis)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w : InfinitePlace K // w.IsReal }
this : normAtComplexPlaces a (↑w : InfinitePlace K) = normAtComplexPlaces x (↑w : InfinitePlace K)
⊢ 0 < x.1 w
have this₁ : a.1 w = x.1 w
Tactic: rw [normAtComplexPlaces_apply_isReal, normAtComplexPlaces_apply_isReal] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
h : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w : InfinitePlace K // w.IsReal }
this : a.1 w = x.1 w
⊢ 0 < x.1 w
have refine_2 : 0 < a.1 w
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (hypothesis)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) A =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
have hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
Tactic: have hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A := by
    refine subset_antisymm (fun x ⟨a, ha₁, ha₂⟩ ↦ ⟨?_, fun w ↦ ?_⟩) (Set.subset_preimage_image _ _)
    · rw [← hA, Set.mem_preimage, ← normAtAllPlaces_eq_of_normAtComplexPlaces_eq ha₂]
      exact Set.mem_image_of_mem normAtAllPlaces (Set.inter_subset_left ha₁)
    · have := funext_iff.mp ha₂ w
      rw [normAtComplexPlaces_apply_isReal, normAtComplexPlaces_apply_isReal] at this
      rw [← this]
      exact ha₁.2 w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
⊢ ((volume : Measure (mixedSpace K)) : (a : Set (mixedSpace K)) → ℝ≥0∞) A =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
have rw : HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in normAtComplexPlaces '' plusPart A,
      ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
  HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
    ∫⁻ (x : realSpace K) in normAtAllPlaces '' A,
      ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
Tactic: rw [volume_eq_two_pow_mul_volume_plusPart hA₁ hm, volume_eq_two_pi_pow_mul_integral hA₃
    (measurableSet_plusPart hm), ← mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
⊢ HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' plusPart A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K)) =
    HPow.hPow (α := ℝ≥0∞) 2 (nrRealPlaces K) * ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' A,
        ∏ w : { w : InfinitePlace K // w.IsComplex }, ENNReal.ofReal (x (↑w : InfinitePlace K))
have refine : normAtComplexPlaces '' plusPart A =ᶠ[ae (F := Measure (realSpace K)) volume] normAtAllPlaces '' A
Tactic: refine congr_arg (_ * _ * ·) <| setLIntegral_congr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
⊢ normAtComplexPlaces '' plusPart A =ᶠ[ae (F := Measure (realSpace K)) volume] normAtAllPlaces '' A
have rw : normAtAllPlaces '' A ∩
    ⋂ (w : { w : InfinitePlace K // w.IsReal }),
      {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} =ᶠ[ae (F := Measure (realSpace K)) volume]
  normAtAllPlaces '' A
Tactic: rw [← volume_eq_two_pow_mul_two_pi_pow_mul_integral_aux hA]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
⊢ normAtAllPlaces '' A ∩
      ⋂ (w : { w : InfinitePlace K // w.IsReal }),
        {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0} =ᶠ[ae (F := Measure (realSpace K)) volume]
    normAtAllPlaces '' A
have refine : ∀ (w : { w : InfinitePlace K // w.IsReal }),
  Eq (α := ℝ≥0∞)
    (((volume : Measure (realSpace K)) : (a : Set (realSpace K)) → ℝ≥0∞)
        {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: refine inter_ae_eq_left_of_ae_eq_univ <| ae_eq_univ.mpr
    <| Set.compl_iInter _ ▸ measure_iUnion_null_iff.mpr fun w ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w : InfinitePlace K // w.IsReal }
⊢ Eq.{u_1 + 1} (α := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}ᶜ
    {x : realSpace K | x (↑w : InfinitePlace K) = 0}
have h : ∀ (x : realSpace K),
  Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}ᶜ x ↔
    Membership.mem (γ := Set (realSpace K)) {x : realSpace K | x (↑w : InfinitePlace K) = 0} x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord (goal)
Goal:
K : Type u_1
inst : Field K
A : Set (mixedSpace K)
inst_1 : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun (w : { w : InfinitePlace K // w.IsReal }) ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w : InfinitePlace K // w.IsReal }
⊢ Eq (α := ℝ≥0∞)
    (((volume : Measure (realSpace K)) : (a : Set (realSpace K)) → ℝ≥0∞)
        {x : realSpace K | x (↑w : InfinitePlace K) ≠ 0}ᶜ :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (((volume : Measure (realSpace K)) : (a : Set (realSpace K)) → ℝ≥0∞)
      {x : realSpace K | x (↑w : InfinitePlace K) = 0} :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: rw [show {x : realSpace K | x w.1 ≠ 0}ᶜ = {x | x w.1 = 0} by ext; simp]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
⊢ ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
have obtain : ∀ (J : ↥(Ideal (𝓞 K))⁰) (hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹),
  ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
Tactic: obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
⊢ ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
have obtain : ∀ (a : 𝓞 K) (ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K)))
  (h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K))
  (h_nm :
    (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
      (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                    (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                      FractionalIdeal (𝓞 K)⁰ K)) :
                ℝ) *
              (4 / π) ^ nrComplexPlaces K *
            (↑(finrank ℚ K)! : ℝ) /
          HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
        √|(↑(discr K) : ℝ)|),
  ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
Tactic: obtain ⟨_, ⟨a, ha, rfl⟩, h_nz, h_nm⟩ :=
    exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr K (FractionalIdeal.mk0 K J)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
⊢ ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
have obtain : ∀ (I₀ : Ideal (𝓞 K)) (hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀),
  ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
Tactic: obtain ⟨I₀, hI⟩ := dvd_iff_le.mpr ((span_singleton_le_iff_mem J).mpr (by exact ha))
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
⊢ I₀ ≠ 0
have contrapose : ∀ (h_nz : I₀ = 0), Eq (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
Tactic: contrapose h_nz
Cleared hypotheses: h_nz
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
h_nz : I₀ = 0
⊢ Eq (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
have hI₁ : a = 0
Tactic: rw [h_nz, mul_zero, zero_eq_bot, span_singleton_eq_bot] at hI
Cleared hypotheses: hI, h_nz
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : a = 0
h_nz : I₀ = 0
⊢ Eq (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
have rw : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
Tactic: rw [Algebra.linearMap_apply, hI, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : a = 0
h_nz : I₀ = 0
rw : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
⊢ Eq (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
have rw₁ : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K) (0 : K)
Tactic: rw [Algebra.linearMap_apply, hI, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : a = 0
h_nz : I₀ = 0
rw : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
rw₁ : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) 0 : K) (0 : K)
⊢ Eq (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
have rw₂ : Eq.{u_1 + 1} (α := K) 0 0
Tactic: rw [Algebra.linearMap_apply, hI, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ClassNumber (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J = C⁻¹
a : 𝓞 K
ha : a ∈ (↑(↑J : Ideal (𝓞 K)) : Set (𝓞 K))
h_nz : Ne (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
h_nm :
  (↑|(Algebra.norm ℚ : (a : K) → ℚ) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)| : ℝ) ≤
    (↑((FractionalIdeal.absNorm : (a : FractionalIdeal (𝓞 K)⁰ K) → ℚ)
                  (↑((FractionalIdeal.mk0 K : (a : ↥(Ideal (𝓞 K))⁰) → (FractionalIdeal (𝓞 K)⁰ K)ˣ) J) :
                    FractionalIdeal (𝓞 K)⁰ K)) :
              ℝ) *
            (4 / π) ^ nrComplexPlaces K *
          (↑(finrank ℚ K)! : ℝ) /
        HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) *
      √|(↑(discr K) : ℝ)|
I₀ : Ideal (𝓞 K)
hI : span {a} = (↑J : Ideal (𝓞 K)) * I₀
⊢ ∃ (I : ↥(Ideal (𝓞 K))⁰),
    (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C ∧
      (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 K))) : ℝ) ≤
        (4 / π) ^ nrComplexPlaces K *
          ((↑(finrank ℚ K)! : ℝ) / HPow.hPow (α := ℝ) (↑(finrank ℚ K) : ℝ) (finrank ℚ K) * √|(↑(discr K) : ℝ)|)
have this : I₀ ≠ 0
Tactic: have : I₀ ≠ 0 := by
    contrapose h_nz
    rw [h_nz, mul_zero, zero_eq_bot, span_singleton_eq_bot] at hI
    rw [Algebra.linearMap_apply, hI, map_zero]