awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
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 }
rw :
  Eq (α := ℝ≥0∞)
    (((volume : Measure (realSpace K)) : (a : Set (realSpace K)) → ℝ≥0∞)
        {x : realSpace K | x (↑w : InfinitePlace K) = 0} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ 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]
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
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∞)

Tactic:
realSpace.volume_eq_zero w.1

Premises used: NumberField.mixedEmbedding.realSpace.volume_eq_zero, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
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∞)

Tactic:
exact realSpace.volume_eq_zero w.1

Premises used: NumberField.mixedEmbedding.realSpace.volume_eq_zero, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ classNumber K ≠ 0

Tactic:
Fintype.card_ne_zero

Premises used: Fintype.card_ne_zero, NumberField.classNumber
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < classNumber K

Tactic:
Fintype.card_pos

Premises used: NumberField.classNumber, Fintype.card_pos
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ classNumber K = 1 ↔ IsPrincipalIdealRing.{u_1} (𝓞 K)

Tactic:
card_classGroup_eq_one_iff

Premises used: card_classGroup_eq_one_iff, NumberField.classNumber
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
C : ClassGroup (𝓞 K)
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) : ℝ)|)
⊢ ∃ (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⁻¹

Premises used: Inv.inv, ClassGroup.mk0_surjective
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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⁻¹
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) : ℝ)|)
⊢ ∃ (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)

Premises used: NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr, DFunLike.coe, rfl, FractionalIdeal.mk0
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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) : ℝ)|
⊢ a ∈ (↑J : Ideal (𝓞 K))

Tactic:
ha

Premises used: Set.Mem
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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) : ℝ)|
⊢ a ∈ (↑J : Ideal (𝓞 K))

Tactic:
exact ha
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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) : ℝ)|
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) : ℝ)|)
⊢ ∃ (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))

Premises used: Iff.mpr, Ideal.dvd_iff_le, Ideal.span_singleton_le_iff_mem
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀
contrapose : ∀ (h_nz : I₀ = 0), Eq (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)
⊢ I₀ ≠ 0

Tactic:
contrapose h_nz
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
⊢ a = 0

Tactic:
rw [h_nz, mul_zero, zero_eq_bot, span_singleton_eq_bot] at hI

Premises used: Ideal.span_singleton_eq_bot, Ideal.zero_eq_bot, MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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
hI₁ : a = 0
⊢ I₀ = 0

Tactic:
rw [h_nz, mul_zero, zero_eq_bot, span_singleton_eq_bot] at hI

Premises used: Ideal.span_singleton_eq_bot, Ideal.zero_eq_bot, MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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)
rw₂ rw₃ : Eq.{u_1 + 1} (α := K) 0 0
⊢ Eq (α := K) ((Algebra.linearMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) (0 : K)

Tactic:
rw [Algebra.linearMap_apply, hI, map_zero]

Premises used: map_zero, Algebra.linearMap_apply
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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

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]
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) 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:
⟨I, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
refine_1 : (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C
refine_2 :
  (↑((absNorm : (a : Ideal (𝓞 K)) → ℕ) (↑I : Ideal (𝓞 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:
refine ⟨I, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀
this_1 : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
this :
  Eq (α := ClassGroup (𝓞 K)) ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I : ClassGroup (𝓞 K))
    (((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ : ClassGroup (𝓞 K))
rw : ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ = C
rw₁ : C⁻¹⁻¹ = C
rw₂ rw₃ : C = C
⊢ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C

Tactic:
rw [this, hJ, inv_inv]

Premises used: inv_inv
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
refine_1 :
  Eq (α := ClassGroup (𝓞 K)) ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I : ClassGroup (𝓞 K))
    (((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ : ClassGroup (𝓞 K))
⊢ (ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I = C

Tactic:
suffices ClassGroup.mk0 I = (ClassGroup.mk0 J)⁻¹ by rw [this, hJ, inv_inv]
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
rw : (↑J : Ideal (𝓞 K)) * (↑I : Ideal (𝓞 K)) = span {a}
rw₁ rw₂ : (↑J : Ideal (𝓞 K)) * (↑I : Ideal (𝓞 K)) = (↑J : Ideal (𝓞 K)) * I₀
⊢ (↑I : Ideal (𝓞 K)) * (↑J : Ideal (𝓞 K)) = span {a}

Tactic:
rw [mul_comm, hI]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.NumberField.ClassNumber
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₀
this : I₀ ≠ 0
I : ↥(Ideal (𝓞 K))⁰ :=
  Subtype.mk (p := fun (x : Ideal (𝓞 K)) ↦ Membership.mem (γ := Submonoid (Ideal (𝓞 K))) (Ideal (𝓞 K))⁰ x) I₀ ⋯
⊢ Eq (α := ClassGroup (𝓞 K)) ((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) I : ClassGroup (𝓞 K))
    (((ClassGroup.mk0 : (a : ↥(Ideal (𝓞 K))⁰) → ClassGroup (𝓞 K)) J)⁻¹ : ClassGroup (𝓞 K))

Tactic:
exact ClassGroup.mk0_eq_mk0_inv_iff.mpr ⟨a, Subtype.coe_ne_coe.1 h_nz, by rw [mul_comm, hI]⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Iff.mp, ClassGroup.mk0_eq_mk0_inv_iff, Subtype.coe_ne_coe