-- Module: Mathlib.NumberTheory.ClassNumber.Finite
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
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
h :
  Fintype.card ι •
      (Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯ *
        y) =
    Fintype.card ι • y *
      Finset.max'
        (Finset.image
          (fun (ijk : ι × ι × ι) ↦
            (abv : (a : R) → ℤ)
              ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
          Finset.univ)
        ⋯
h₁ :
  Fintype.card ι •
      (Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯ *
        y) =
    Fintype.card ι •
      (y *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯)
h₂ : ℤ
h₃ :
  Fintype.card ι •
      (y *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯) =
    Fintype.card ι •
      (y *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯)
h₄ : ℤ
h₅ :
  Fintype.card ι •
      (y *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯) =
    Fintype.card ι •
      (y *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯)
h₆ : ℤ
⊢ Fintype.card ι •
      (Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯ *
        y) =
    Finset.card.{u_5} (α := ι) Finset.univ • y *
      Finset.max'
        (Finset.image
          (fun (ijk : ι × ι × ι) ↦
            (abv : (a : R) → ℤ)
              ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
          Finset.univ)
        ⋯

Tactic:
rw [Finset.card_univ, smul_mul_assoc, mul_comm]

Premises used: Finset.card_univ, smul_mul_assoc, mul_comm