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
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) (0 : S)

Tactic:
mt ((injective_iff_map_eq_zero _).mp bS.algebraMap_injective _) ?_

Premises used: Module.Basis.algebraMap_injective, mt, injective_iff_map_eq_zero, Iff.mp
-- 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
refine : ¬Eq (α := R) (∏ m ∈ finsetApprox bS adm, m) 0
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) (0 : S)

Tactic:
refine mt ((injective_iff_map_eq_zero _).mp bS.algebraMap_injective _) ?_

Premises used: Module.Basis.algebraMap_injective, mt, injective_iff_map_eq_zero, Iff.mp
-- 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
simp : ∀ (x : R), ¬(x ∈ finsetApprox bS adm ∧ x = 0)
⊢ ¬Eq (α := R) (∏ m ∈ finsetApprox bS adm, m) 0

Tactic:
simp only [Finset.prod_eq_zero_iff, not_exists]

Premises used: not_exists, Finset.prod_eq_zero_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
hx : 0 ∈ finsetApprox bS adm
⊢ False

Tactic:
finsetApprox.zero_notMem bS adm hx

Premises used: ClassGroup.finsetApprox.zero_notMem
-- 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
hx : 0 ∈ finsetApprox bS adm
⊢ False

Tactic:
exact finsetApprox.zero_notMem bS adm hx

Premises used: ClassGroup.finsetApprox.zero_notMem
-- 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
J : Ideal S
h : Membership.mem (α := S) J ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)
⊢ J ≠ ⊥

Tactic:
(Submodule.ne_bot_iff _).mpr ⟨_, h, prod_finsetApprox_ne_zero _ _⟩

Premises used: Iff.mpr, And.intro, Submodule.ne_bot_iff, Exists.intro, ClassGroup.prod_finsetApprox_ne_zero
-- 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)⁰
set :
  let M : R := ∏ m ∈ finsetApprox bS adm, m;
  ∃ (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)
⊢ ∃ (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 ∈ finsetApprox bS adm, m) : S)

Tactic:
set M := ∏ m ∈ finsetApprox bS adm, m

Premises used: ClassGroup.finsetApprox
-- 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
⊢ Ne.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) M : S) (0 : S)

Tactic:
have hM : algebraMap R S M ≠ 0 := prod_finsetApprox_ne_zero bS adm
-- 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)
obtain :
  ∀ (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)⁰),
      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)
⊢ ∃ (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:
obtain ⟨b, b_mem, b_ne_zero, b_min⟩ := exists_min abv I

Premises used: ClassGroup.exists_min
-- 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
this : Ideal.span {b} ∣ Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S)
obtain :
  ∀ (J : Ideal S)
    (hJ : Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = Ideal.span {b} * J),
    ∃ (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)
⊢ ∃ (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:
obtain ⟨J, hJ⟩ := this
-- 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
⊢ ∃ (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:
⟨⟨J, ?_⟩, ?_, ?_⟩

Premises used: Subtype.mk, And.intro, Exists.intro
-- 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
refine_1 : Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ J
refine_2 :
  Eq (α := ClassGroup S) ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S) I : ClassGroup S)
    ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) :
      ClassGroup S)
refine_3 :
  Membership.mem (α := S)
    (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) : Ideal S)
    ((algebraMap R S : (a : R) → S) M : 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:
refine ⟨⟨J, ?_⟩, ?_, ?_⟩
-- 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
refine_1 : J ≠ 0
⊢ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ J

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero]

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- 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
hJ :
  Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) =
    HMul.hMul (α := Ideal S) (Ideal.span {b}) 0
⊢ Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = ⊥

Tactic:
rw [Ideal.zero_eq_bot, Ideal.mul_bot] at hJ

Premises used: Ideal.mul_bot, Ideal.zero_eq_bot
-- 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
hJ : Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = ⊥
⊢ False

Tactic:
hM (Ideal.span_singleton_eq_bot.mp (I.2.2 _ hJ))

Premises used: Ideal.span_singleton_eq_bot, And.right, Iff.mp, Subtype.property
-- 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
hJ : Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S) = ⊥
⊢ False

Tactic:
exact hM (Ideal.span_singleton_eq_bot.mp (I.2.2 _ hJ))

Premises used: Ideal.span_singleton_eq_bot, And.right, Iff.mp, Subtype.property
-- 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
refine_2 :
  ∃ (x : S) (y : S) (_ : x ≠ 0) (_ : y ≠ 0),
    Ideal.span {x} * (↑I : Ideal S) =
      Ideal.span {y} *
        (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) : Ideal S)
⊢ Eq (α := ClassGroup S) ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S) I : ClassGroup S)
    ((mk0 : (a : ↥(Ideal S)⁰) → ClassGroup S)
        (Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) :
      ClassGroup S)

Tactic:
rw [ClassGroup.mk0_eq_mk0_iff]

Premises used: ClassGroup.mk0_eq_mk0_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
⊢ ∃ (x : S) (y : S) (_ : x ≠ 0) (_ : y ≠ 0),
    Ideal.span {x} * (↑I : Ideal S) =
      Ideal.span {y} *
        (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) : Ideal S)

Tactic:
⟨algebraMap _ _ M, b, hM, b_ne_zero, hJ⟩

Premises used: Algebra.algebraMap, Exists.intro, DFunLike.coe
-- 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
⊢ ∃ (x : S) (y : S) (_ : x ≠ 0) (_ : y ≠ 0),
    Ideal.span {x} * (↑I : Ideal S) =
      Ideal.span {y} *
        (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) : Ideal S)

Tactic:
exact ⟨algebraMap _ _ M, b, hM, b_ne_zero, hJ⟩
-- 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
refine_3 :
  (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) : Ideal S) ∣
    Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S))
⊢ Membership.mem (α := S)
    (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) : Ideal S)
    ((algebraMap R S : (a : R) → S) M : S)

Tactic:
rw [← SetLike.mem_coe, ← Set.singleton_subset_iff, ← Ideal.span_le, ← Ideal.dvd_iff_le]

Premises used: Ideal.span_le, Ideal.dvd_iff_le, Set.singleton_subset_iff, SetLike.mem_coe
-- 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 S
apply₁ : Ne (α := Ideal S) (Ideal.span {b}) 0
apply₂ :
  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)))
⊢ (↑(Subtype.mk (p := fun (x : Ideal S) ↦ Membership.mem (γ := Submonoid (Ideal S)) (Ideal S)⁰ x) J ⋯) : Ideal S) ∣
    Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S))

Tactic:
apply (mul_dvd_mul_iff_left _).mp _

Premises used: mul_dvd_mul_iff_left, Iff.mp
-- 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
⊢ Ne (α := Ideal S) (Ideal.span {b}) 0

Tactic:
mt Ideal.span_singleton_eq_bot.mp b_ne_zero

Premises used: Ideal.span_singleton_eq_bot, mt, Iff.mp
-- 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
⊢ Ne (α := Ideal S) (Ideal.span {b}) 0

Tactic:
exact mt Ideal.span_singleton_eq_bot.mp b_ne_zero

Premises used: Ideal.span_singleton_eq_bot, mt, Iff.mp