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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
rw : Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0
⊢ (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
have h : Ne (α := ℝ) (↑(Fintype.card ι) : ℝ) 0
Tactic: rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel₀, rpow_neg_one,
      mul_left_comm, mul_inv_cancel₀, mul_one, rpow_natCast]
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
rw : Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0
h : Ne (α := ℝ) (↑(Fintype.card ι) : ℝ) 0
⊢ (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
have hx : LE.le (α := ℝ) 0 (↑(normBound abv bS) : ℝ)
Tactic: rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel₀, rpow_neg_one,
      mul_left_comm, mul_inv_cancel₀, mul_one, rpow_natCast]
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
rw : Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0
h : Ne (α := ℝ) (↑(Fintype.card ι) : ℝ) 0
hx : LE.le (α := ℝ) 0 (↑(normBound abv bS) : ℝ)
⊢ (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
have hx₁ : LE.le (α := ℝ) 0 (↑((abv : (a : R) → ℤ) b) : ℝ)
Tactic: rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel₀, rpow_neg_one,
      mul_left_comm, mul_inv_cancel₀, mul_one, rpow_natCast]
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
rw : Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0
h : Ne (α := ℝ) (↑(Fintype.card ι) : ℝ) 0
hx : LE.le (α := ℝ) 0 (↑(normBound abv bS) : ℝ)
hx₁ : LE.le (α := ℝ) 0 (↑((abv : (a : R) → ℤ) b) : ℝ)
⊢ (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
have hy : 0 ≤ HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
Tactic: rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel₀, rpow_neg_one,
      mul_left_comm, mul_inv_cancel₀, mul_one, rpow_natCast]
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
⊢ Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0
have norm_cast : ¬normBound abv bS = 0
Tactic: norm_cast
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
⊢ Ne (α := ℝ) (↑(normBound abv bS) : ℝ) 0
have try : ¬normBound abv bS = 0
Tactic: try norm_cast; lia
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
⊢ Ne (α := ℝ) (↑(Fintype.card ι) : ℝ) 0
have h : ¬Fintype.card ι = 0
Tactic: norm_cast
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
⊢ Ne (α := ℝ) (↑(Fintype.card ι) : ℝ) 0
have h : ¬Fintype.card ι = 0
Tactic: try norm_cast; lia
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
⊢ LE.le (α := ℝ) 0 (↑(normBound abv bS) : ℝ)
have hx : 0 ≤ normBound abv bS
Tactic: norm_cast
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
⊢ LE.le (α := ℝ) 0 (↑(normBound abv bS) : ℝ)
have hx : 0 ≤ normBound abv bS
Tactic: try norm_cast; lia
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
this_1 : 0 < normBound abv bS
this : LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) b : ℤ)
⊢ 0 ≤ HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
have linarith : HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ)) < 0 →
  0 - ε +
      (1 * HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ)) -
        HMul.hMul (α := ℝ) 1 0) =
    0
Tactic: linarith
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - b • q) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b : S) : R) : ℤ)
have ε_le : (↑(normBound abv bS) : ℝ) *
    HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
  HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
Tactic: have ε_le : (normBound abv bS : ℝ) * (abv b • ε) ^ (Fintype.card ι : ℝ)
                ≤ abv b ^ (Fintype.card ι : ℝ) := by
    have := normBound_pos abv bS
    have := abv.nonneg b
    rw [ε_eq, Algebra.smul_def, eq_intCast, mul_rpow, ← rpow_mul, div_mul_cancel₀, rpow_neg_one,
      mul_left_comm, mul_inv_cancel₀, mul_one, rpow_natCast] <;>
      try norm_cast; lia
    · exact Int.cast_nonneg this
    · linarith
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - b • q) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b : S) : R) : ℤ)
have s_eq : ∀ (i : ι),
  Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
Tactic: have s_eq : ∀ i, s i = bS.repr a i := fun i => rfl
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - b • q) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b : S) : R) : ℤ)
have r_eq : ∀ (j : Fin (cardM bS adm).succ) (i : ι),
  rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
Tactic: have r_eq : ∀ j i, rs j i = μ j * s i % b := fun i j => rfl
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
r_eq :
  ∀ (j : Fin (cardM bS adm).succ) (i : ι),
    rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
i : ι
j : Fin (cardM bS adm).succ
rw :
  HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
    b * qs j i +
      HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
⊢ HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
    b * qs j i + rs j i
have rw₁ : HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
  HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R)
Tactic: rw [r_eq, EuclideanDomain.div_add_mod]
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
r_eq :
  ∀ (j : Fin (cardM bS adm).succ) (i : ι),
    rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - b • q) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b : S) : R) : ℤ)
have μ_eq : ∀ (i : ι) (j : Fin (cardM bS adm).succ),
  HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
    b * qs j i + rs j i
Tactic: have μ_eq : ∀ i j, μ j * s i = b * qs j i + rs j i := by
    intro i j
    rw [r_eq, EuclideanDomain.div_add_mod]
-- 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
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
r_eq :
  ∀ (j : Fin (cardM bS adm).succ) (i : ι),
    rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
μ_eq :
  ∀ (i : ι) (j : Fin (cardM bS adm).succ),
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
      b * qs j i + rs j i
j : Fin (cardM bS adm).succ
⊢ HSMul.hSMul (α := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) a =
    HSMul.hSMul (β := S) b (∑ i : ι, HSMul.hSMul (β := S) (qs j i) ((bS : (a : ι) → S) i : S)) +
      ∑ i : ι, HSMul.hSMul (β := S) (rs j i) ((bS : (a : ι) → S) i : S)
have rw : HSMul.hSMul (α := R) (β := S) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R)
    (∑ i : ι,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
        ((bS : (a : ι) → S) i : S)) =
  HSMul.hSMul (β := S) b (∑ i : ι, HSMul.hSMul (β := S) (qs j i) ((bS : (a : ι) → S) i : S)) +
    ∑ i : ι, HSMul.hSMul (β := S) (rs j i) ((bS : (a : ι) → S) i : S)
Tactic: rw [← bS.sum_repr a]