-- 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
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
rw :
  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) ((s : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S)) =
    b •
        HSMul.hSMul (β := S)
          (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
              ((s : (a : ι) → R) i : R) /
            b)
          ((bS : (a : ι) → S) i : S) +
      HSMul.hSMul (β := S)
        (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
            ((s : (a : ι) → R) i : R) %
          b)
        ((bS : (a : ι) → S) i : S)
⊢ 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) i : R)
        ((bS : (a : ι) → S) i : S)) =
    b •
        HSMul.hSMul (β := S)
          (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
              ((s : (a : ι) → R) i : R) /
            b)
          ((bS : (a : ι) → S) i : S) +
      HSMul.hSMul (β := S)
        (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
            ((s : (a : ι) → R) i : R) %
          b)
        ((bS : (a : ι) → S) i : S)
have rw₁ : HSMul.hSMul (β := S)
    (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
      ((s : (a : ι) → R) i : R))
    ((bS : (a : ι) → S) i : S) =
  b •
      HSMul.hSMul (β := S)
        (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
            ((s : (a : ι) → R) i : R) /
          b)
        ((bS : (a : ι) → S) i : S) +
    HSMul.hSMul (β := S)
      (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
          ((s : (a : ι) → R) i : R) %
        b)
      ((bS : (a : ι) → S) i : S)
Tactic: rw [← s_eq, ← mul_smul, μ_eq, add_smul, mul_smul, ← μ_eq]