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 < ε
ε_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) (β := 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)
have simp : Eq.{u_2 + 1} (α := S)
  (∑ x : ι,
    HSMul.hSMul (α := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
      (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) x : R)
        ((bS : (a : ι) → S) x : S)))
  (∑ x : ι,
    (b •
        HSMul.hSMul (β := S)
          (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
              ((s : (a : ι) → R) x : R) /
            b)
          ((bS : (a : ι) → S) x : S) +
      HSMul.hSMul (β := S)
        (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
            ((s : (a : ι) → R) x : R) %
          b)
        ((bS : (a : ι) → S) x : S)))
Tactic: simp only [μ, qs, rs, Finset.smul_sum, ← Finset.sum_add_distrib]
-- 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
μ_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
⊢ ∃ (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 μ_mul_a_eq : ∀ (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)
Tactic: have μ_mul_a_eq : ∀ j, μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i := by
    intro j
    rw [← bS.sum_repr a]
    simp only [μ, qs, rs, Finset.smul_sum, ← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [← s_eq, ← mul_smul, μ_eq, add_smul, mul_smul, ← μ_eq]
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      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) : ℤ)
have obtain : ∀ (a' : S) (b' : R) (hb' : b' ≠ 0) (h : b' • a = b * a'),
  ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      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) : ℤ)
Tactic: obtain ⟨a', b', hb', h⟩ := Algebra.IsAlgebraic.exists_smul_eq_mul R a hb
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      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) : ℤ)
have obtain : ∀ (q : S) (r : R) (hr : r ∈ finsetApprox bS adm)
  (hqr :
    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) : ℤ)),
  ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      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) : ℤ)
Tactic: obtain ⟨q, r, hr, hqr⟩ := exists_mem_finsetApprox bS adm a' hb'
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  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) : ℤ)
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      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) : ℤ)
have refine : 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) : ℤ)
Tactic: refine ⟨q, r, 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  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) : ℤ)
⊢ 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) : ℤ)
have lt_of_mul_lt_mul_left : HMul.hMul (α := ℤ) (β := ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) <
  HMul.hMul (α := ℤ) (β := ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
Tactic: refine
    lt_of_mul_lt_mul_left ?_ (show 0 ≤ abv (Algebra.norm R (algebraMap R S b')) from abv.nonneg _)
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  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) : ℤ)
⊢ HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) <
    HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
have lt_of_le_of_lt : HMul.hMul (α := ℤ) (β := ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) =
  HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
Tactic: refine
    lt_of_le_of_lt (le_of_eq ?_)
      (mul_lt_mul hqr le_rfl (abv.pos ((Algebra.norm_ne_zero_iff_of_basis bS).mpr hb))
        (abv.nonneg _))
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  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) : ℤ)
⊢ HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
have rw : (abv : (a : R) → ℤ)
    (HMul.hMul (α := R) (β := R) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R)
      ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R)) =
  HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
Tactic: rw [← abv.map_mul, ← map_mul, ← abv.map_mul, ← map_mul, ← Algebra.smul_def,
    smul_sub b', sub_mul, smul_comm, h, mul_comm b a', Algebra.smul_mul_assoc r a' b,
    Algebra.smul_mul_assoc b' q b]
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  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) : ℤ)
rw :
  (abv : (a : R) → ℤ)
      (HMul.hMul (α := R) (β := R) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R)
        ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R)) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
have rw₁ : (abv : (a : R) → ℤ)
    ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) : R) =
  HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
Tactic: rw [← abv.map_mul, ← map_mul, ← abv.map_mul, ← map_mul, ← Algebra.smul_def,
    smul_sub b', sub_mul, smul_comm, h, mul_comm b a', Algebra.smul_mul_assoc r a' b,
    Algebra.smul_mul_assoc b' q b]
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  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) : ℤ)
rw :
  (abv : (a : R) → ℤ)
      (HMul.hMul (α := R) (β := R) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R)
        ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R)) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
rw₁ :
  (abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) :
        R) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
have rw₂ : Eq (α := ℤ)
  ((abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) :
        R) :
    ℤ)
  ((abv : (a : R) → ℤ)
      (HMul.hMul (α := R) (β := R) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R)
        ((Algebra.norm R : (a : S) → R) b : R)) :
    ℤ)
Tactic: rw [← abv.map_mul, ← map_mul, ← abv.map_mul, ← map_mul, ← Algebra.smul_def,
    smul_sub b', sub_mul, smul_comm, h, mul_comm b a', Algebra.smul_mul_assoc r a' b,
    Algebra.smul_mul_assoc b' q b]
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  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) : ℤ)
rw :
  (abv : (a : R) → ℤ)
      (HMul.hMul (α := R) (β := R) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R)
        ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R)) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
rw₁ :
  (abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) :
        R) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
rw₂ :
  Eq (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) :
          R) :
      ℤ)
    ((abv : (a : R) → ℤ)
        (HMul.hMul (α := R) (β := R) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R)
          ((Algebra.norm R : (a : S) → R) b : R)) :
      ℤ)
⊢ HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
have rw₃ : Eq (α := ℤ)
  ((abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) :
        R) :
    ℤ)
  ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((r • a' - b' • q) * b) : R) : ℤ)
Tactic: rw [← abv.map_mul, ← map_mul, ← abv.map_mul, ← map_mul, ← Algebra.smul_def,
    smul_sub b', sub_mul, smul_comm, h, mul_comm b a', Algebra.smul_mul_assoc r a' b,
    Algebra.smul_mul_assoc b' q b]
-- 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 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  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) : ℤ)
rw :
  (abv : (a : R) → ℤ)
      (HMul.hMul (α := R) (β := R) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R)
        ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R)) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
rw₁ :
  (abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) :
        R) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
rw₂ :
  Eq (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) :
          R) :
      ℤ)
    ((abv : (a : R) → ℤ)
        (HMul.hMul (α := R) (β := R) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R)
          ((Algebra.norm R : (a : S) → R) b : R)) :
      ℤ)
rw₃ :
  Eq (α := ℤ)
    ((abv : (a : R) → ℤ)
        ((Algebra.norm R : (a : S) → R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) b' : S) (r • a - q * b)) :
          R) :
      ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((r • a' - b' • q) * b) : R) : ℤ)
⊢ HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
have rw₄ : Eq (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (b' • (r • a - q * b)) : R) : ℤ)
  ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((r • a' - b' • q) * b) : R) : ℤ)
Tactic: rw [← abv.map_mul, ← map_mul, ← abv.map_mul, ← map_mul, ← Algebra.smul_def,
    smul_sub b', sub_mul, smul_comm, h, mul_comm b a', Algebra.smul_mul_assoc r a' b,
    Algebra.smul_mul_assoc b' q b]