awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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)⁰),
    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)
have suffices : Ideal.span {b} ∣ Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal 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
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
⊢ Ideal.span {b} ∣ Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) M : S)) * (↑I : Ideal S)
have 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)
Tactic: rw [Ideal.dvd_iff_le, Ideal.mul_le]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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)
⊢ Membership.mem (γ := Ideal S) (Ideal.span {b}) (r' * a)
have rw : ∀ (hr' : (algebraMap R S : (a : R) → S) M ∣ r') (a : S) (ha : a ∈ (↑I : Ideal S)), b ∣ r' * a
Tactic: rw [Ideal.mem_span_singleton] at hr' ⊢
Cleared hypotheses: hr', a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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)
⊢ b ∣ r' * a
have 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
Tactic: obtain ⟨q, r, r_mem, lt⟩ := exists_mem_finset_approx' bS adm a b_ne_zero
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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) : ℤ)
⊢ b ∣ r' * a
have h : q * b ∣ r' * a
Tactic: apply @dvd_of_mul_left_dvd _ _ q
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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) : ℤ)
⊢ q * b ∣ r' * a
have 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) : ℤ)
Tactic: simp only [Algebra.smul_def] at lt
Cleared hypotheses: lt
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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) : ℤ)
⊢ q * b ∣ r' * a
have h : HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) a ∣ 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)]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
have h : r ∣ M
Tactic: refine mul_dvd_mul_right (dvd_trans (map_dvd _ ?_) hr') _
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
⊢ ∃ (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'
have 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)
Tactic: obtain ⟨⟨I, hI⟩, rfl⟩ := ClassGroup.mk0_surjective I'
Cleared hypotheses: I'
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨J, mk0_eq_mk0, J_dvd⟩ := exists_mk0_eq_mk0 bS adm ⟨I, hI⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsDedekindDomain S
inst_18 : Algebra.IsAlgebraic R S
⊢ Ne (α := Ideal S)
    (Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S))) 0
have rw : ¬Eq.{u_2 + 1} (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) (0 : S)
Tactic: rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsDedekindDomain S
inst_18 : Algebra.IsAlgebraic R S
I : Ideal S
⊢ Ideal.span (singleton (α := S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)) ≤ I ↔
    Membership.mem (α := S) (γ := Ideal S) ((Equiv.refl (Ideal S) : (a : Ideal S) → Ideal S) I : Ideal S)
      ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)
have rw : Membership.mem (α := S) (↑I : Set S) ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S) ↔
  Membership.mem (α := S) I ((algebraMap R S : (a : R) → S) (∏ m ∈ finsetApprox bS adm, m) : S)
Tactic: rw [Equiv.refl_apply, Ideal.span_le, Set.singleton_subset_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
⊢ Fintype (ClassGroup S)
have choose : (s : Finset L) →
  (b : Basis (↥s) K L) →
    (hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)) → Fintype (ClassGroup S)
Tactic: choose s b hb_int using FiniteDimensional.exists_is_basis_integral R K L
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
⊢ LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b :
          Basis (↥s) K L) :
      (a : ↥s) → L)
have apply : Function.Injective.{u_1 + 1, u_3 + 1} (β := K) fun (r : R) ↦ HSMul.hSMul (β := K) r 1
Tactic: apply (Basis.linearIndependent _).restrict_scalars
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
⊢ Function.Injective.{u_1 + 1, u_3 + 1} (β := K) fun (r : R) ↦ HSMul.hSMul (β := K) r 1
have simp : Function.Injective.{u_1 + 1, u_3 + 1} (β := K) fun (r : R) ↦ (algebraMap R K : (a : R) → K) r
Tactic: simp only [Algebra.smul_def, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
⊢ Fintype (ClassGroup S)
have this₁ : LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
  (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) sorry b :
        Basis (↥s) K L) :
    (a : ↥s) → L)
Tactic: have : LinearIndependent R ((Algebra.traceForm K L).dualBasis
      (traceForm_nondegenerate K L) b) := by
    apply (Basis.linearIndependent _).restrict_scalars
    simp only [Algebra.smul_def, mul_one]
    apply IsFractionRing.injective
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this_3 : IsDedekindDomain S := ⋯
s : Finset L
b : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b : (a : ↥s) → L) x : L)
this :
  LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b :
          Basis (↥s) K L) :
      (a : ↥s) → L)
⊢ Fintype (ClassGroup S)
have obtain : (n : ℕ) →
  (b :
      Basis.{0, u_1, u_4} (Fin n) R
        ↥(LinearMap.range
            ((↑R :
                {S M : Type u_2} →
                  {M₂ : Type u_4} →
                    [inst : Semiring R] →
                      [inst_18 : Semiring S] →
                        [inst_19 : AddCommMonoid M] →
                          [inst_20 : AddCommMonoid M₂] →
                            [inst_21 : Module R M] →
                              [inst_22 : Module R M₂] →
                                [inst_23 : Module S M] →
                                  [inst_24 : Module S M₂] →
                                    [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
              (Algebra.linearMap S L)))) →
    Fintype (ClassGroup S)
Tactic: obtain ⟨n, b⟩ :=
    Submodule.basisOfPidOfLESpan this (IsIntegralClosure.range_le_span_dualBasis S b hb_int)