-- 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) : ℤ)
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) : ℤ)
rw₅ :
  Eq (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (b' • r • a - b' • (q * b)) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((r • a' - b' • q) * b) : R) : ℤ)
rw₆ :
  Eq (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (b' • r • a - b' • (q * b)) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' * b - b' • q * b) : R) : ℤ)
rw₇ :
  Eq (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • b' • a - b' • (q * b)) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' * b - b' • q * b) : R) : ℤ)
rw₈ :
  Eq (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • (b * a') - b' • (q * b)) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' * b - 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) (r • (a' * b) - b' • (q * b)) : R) : ℤ)
  ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' * b - 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]