awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
J : Ideal S
hJ : Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = Ideal.span {b} * J
rw :
  HMul.hMul (α := Ideal S) (Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S))) (Ideal.span {b}) ≤
    Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S)
⊢ Ideal.span {b} *
      (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) : Ideal S) ∣
    HMul.hMul (α := Ideal S) (Ideal.span {b}) (Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)))

Tactic:
rw [Subtype.coe_mk, Ideal.dvd_iff_le, ← hJ, mul_comm]

Premises used: Subtype.coe_mk, Ideal.dvd_iff_le, mul_comm
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
J : Ideal S
hJ : Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = Ideal.span {b} * J
apply : Ideal.span {b} ≤ (↑I : Ideal S)
⊢ HMul.hMul (α := Ideal S) (Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S))) (Ideal.span {b}) ≤
    Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S)

Tactic:
apply Ideal.mul_mono le_rfl

Premises used: le_rfl, Ideal.mul_mono
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
J : Ideal S
hJ : Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = Ideal.span {b} * J
rw : b ∈ (↑(↑I : Ideal S) : Set S)
⊢ Ideal.span {b} ≤ (↑I : Ideal S)

Tactic:
rw [Ideal.span_le, Set.singleton_subset_iff]

Premises used: Ideal.span_le, Set.singleton_subset_iff
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
J : Ideal S
hJ : Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = Ideal.span {b} * J
⊢ b ∈ (↑(↑I : Ideal S) : Set S)

Tactic:
b_mem
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
J : Ideal S
hJ : Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = Ideal.span {b} * J
⊢ b ∈ (↑(↑I : Ideal S) : Set S)

Tactic:
exact b_mem
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
suffices : Ideal.span {b} ∣ Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S)
⊢ ∃ (J : ↥(Ideal S)⁰),
    Eq (α := ClassGroup S) ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S) I : ClassGroup S)
        ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S) J : ClassGroup S) ∧
      Membership.mem (α := S) (↑J : Ideal S) ((algebraMap R S : (a : R) → S) M : S)

Tactic:
suffices Ideal.span {b} ∣ Ideal.span {algebraMap _ _ M} * I.1 by
    obtain ⟨J, hJ⟩ := this
    refine ⟨⟨J, ?_⟩, ?_, ?_⟩
    · rw [mem_nonZeroDivisors_iff_ne_zero]
      rintro rfl
      rw [Ideal.zero_eq_bot, Ideal.mul_bot] at hJ
      exact hM (Ideal.span_singleton_eq_bot.mp (I.2.2 _ hJ))
    · rw [ClassGroup.mk0_eq_mk0_iff]
      exact ⟨algebraMap _ _ M, b, hM, b_ne_zero, hJ⟩
    rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ← Ideal.dvd_iff_le]
    apply (mul_dvd_mul_iff_left _).mp _
    swap; · exact mt Ideal.span_singleton_eq_bot.mp b_ne_zero
    rw [Subtype.coe_mk, Ideal.dvd_iff_le, ← hJ, mul_comm]
    apply Ideal.mul_mono le_rfl
    rw [Ideal.span_le, Set.singleton_subset_iff]
    exact b_mem
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
rw :
  ∀ (r : S),
    Membership.mem (γ := Ideal S) (Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S))) r →
      ∀ s ∈ (↑I : Ideal S), Membership.mem (γ := Ideal S) (Ideal.span {b}) (r * s)
⊢ Ideal.span {b} ∣ Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S)

Tactic:
rw [Ideal.dvd_iff_le, Ideal.mul_le]

Premises used: Ideal.dvd_iff_le, Ideal.mul_le
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : Membership.mem (γ := Ideal S) (Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S))) r'
a : S
ha : a ∈ (↑I : Ideal S)
rw : ∀ (hr' : (algebraMap R S : (a : R) → S) M ∣ r') (a : S) (ha : a ∈ (↑I : Ideal S)), b ∣ r' * a
⊢ Membership.mem (γ := Ideal S) (Ideal.span {b}) (r' * a)

Tactic:
rw [Ideal.mem_span_singleton] at hr' ⊢

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : (algebraMap R S : (a : R) → S) M ∣ r'
a : S
ha : a ∈ (↑I : Ideal S)
obtain :
  ∀ (q : S) (r : R) (r_mem : r ∈ finsetApprox bS adm)
    (lt :
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)),
    b ∣ r' * a
⊢ b ∣ r' * a

Tactic:
obtain ⟨q, r, r_mem, lt⟩ := exists_mem_finset_approx' bS adm a b_ne_zero

Premises used: ClassGroup.exists_mem_finset_approx'
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : (algebraMap R S : (a : R) → S) M ∣ r'
a : S
ha : a ∈ (↑I : Ideal S)
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
h : q * b ∣ r' * a
⊢ b ∣ r' * a

Tactic:
apply @dvd_of_mul_left_dvd _ _ q

Premises used: dvd_of_mul_left_dvd
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : (algebraMap R S : (a : R) → S) M ∣ r'
a : S
ha : a ∈ (↑I : Ideal S)
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ LT.lt (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a - q * b) : R) :
      ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
simp only [Algebra.smul_def] at lt

Premises used: Algebra.smul_def
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : (algebraMap R S : (a : R) → S) M ∣ r'
a : S
ha : a ∈ (↑I : Ideal S)
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt :
  LT.lt (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a - q * b) : R) :
      ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
h : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a ∣ r' * a
⊢ q * b ∣ r' * a

Tactic:
rw [←
    sub_eq_zero.mp (b_min _ (I.1.sub_mem (I.1.mul_mem_left _ ha) (I.1.mul_mem_left _ b_mem)) lt)]

Premises used: sub_eq_zero, Iff.mp, Ideal.sub_mem, Ideal.mul_mem_left, Subtype.val
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : (algebraMap R S : (a : R) → S) M ∣ r'
a : S
ha : a ∈ (↑I : Ideal S)
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt :
  LT.lt (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a - q * b) : R) :
      ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a ∣ r' * a

Tactic:
mul_dvd_mul_right (dvd_trans (map_dvd _ ?_) hr') _

Premises used: mul_dvd_mul_right, dvd_trans, map_dvd
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : (algebraMap R S : (a : R) → S) M ∣ r'
a : S
ha : a ∈ (↑I : Ideal S)
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt :
  LT.lt (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a - q * b) : R) :
      ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
h : r ∣ M
⊢ HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a ∣ r' * a

Tactic:
refine mul_dvd_mul_right (dvd_trans (map_dvd _ ?_) hr') _

Premises used: mul_dvd_mul_right, dvd_trans, map_dvd
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : (algebraMap R S : (a : R) → S) M ∣ r'
a : S
ha : a ∈ (↑I : Ideal S)
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt :
  LT.lt (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a - q * b) : R) :
      ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ r ∣ M

Tactic:
Multiset.dvd_prod (Multiset.mem_map.mpr ⟨_, r_mem, rfl⟩)

Premises used: Iff.mpr, Multiset.mem_map, Multiset.dvd_prod, Finset.prod, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : ↥(Ideal S)⁰
M : R := ∏ m ∈ finsetApprox bS adm, m
hM : Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
b_min :
  ∀ c ∈ (↑I : Ideal S),
    LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) c : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ) →
      c = 0
r' : S
hr' : (algebraMap R S : (a : R) → S) M ∣ r'
a : S
ha : a ∈ (↑I : Ideal S)
q : S
r : R
r_mem : r ∈ finsetApprox bS adm
lt :
  LT.lt (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a - q * b) : R) :
      ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ r ∣ M

Tactic:
exact Multiset.dvd_prod (Multiset.mem_map.mpr ⟨_, r_mem, rfl⟩)

Premises used: Iff.mpr, Multiset.mem_map, Multiset.dvd_prod, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I' : ClassGroup S
obtain :
  ∀ (I : Ideal S) (hI : Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I),
    ∃ (a :
      { J : Ideal S // Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) }),
      mkMMem bS adm a =
        (mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
          (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) I hI)
⊢ ∃ (a :
    { J : Ideal S // Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) }),
    mkMMem bS adm a = I'

Tactic:
obtain ⟨⟨I, hI⟩, rfl⟩ := ClassGroup.mk0_surjective I'

Premises used: ClassGroup.mk0_surjective, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : IsDedekindDomain S
inst_9 : Algebra.IsAlgebraic R S
I : Ideal S
hI : Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ I
obtain :
  ∀ (J : ↥(Ideal S)⁰)
    (mk0_eq_mk0 :
      Eq (α := ClassGroup S)
        ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
            (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) I hI) :
          ClassGroup S)
        ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S) J : ClassGroup S))
    (J_dvd :
      Membership.mem (α := S) (↑J : Ideal S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)),
    ∃ (a :
      { J : Ideal S // Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) }),
      mkMMem bS adm a =
        (mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
          (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) I hI)
⊢ ∃ (a :
    { J : Ideal S // Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) }),
    mkMMem bS adm a =
      (mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) I hI)

Tactic:
obtain ⟨J, mk0_eq_mk0, J_dvd⟩ := exists_mk0_eq_mk0 bS adm ⟨I, hI⟩

Premises used: Subtype.mk, ClassGroup.exists_mk0_eq_mk0