-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
I : Type u_4
inst_3 : DecidableEq I
b : Basis I R S
f : I →₀ S
x : S
a : (i : I) → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
h₁ :
  ∀ (k : I),
    Eq (α := S ⊗[R] S)
      (Finsupp.sum
        (f.sum fun (i : I) (y : S) ↦
          HSMul.hSMul (α := R) (β := I →₀ R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            ((b.repr : (a : S) → I →₀ R) y : I →₀ R))
        fun (j : I) (z : R) ↦ HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
      (f.sum fun (i : I) (y : S) ↦
        Finsupp.sum ((b.repr : (a : S) → I →₀ R) y) fun (j : I) (z : R) ↦
          HSMul.hSMul.{u_1, u_2, u_2} (α := R)
            ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R) : (a : I) → R) k :
              R)
            (HSMul.hSMul (β := S ⊗[R] S) z ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S)))
h₂ :
  ∀ (x : S),
    ∑ a ∈ Finsupp.support.{u_4, u_1} (M := R) ((b.repr : (a : S) → I →₀ R) x),
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((b.repr : (a : S) → I →₀ R) x : I →₀ R) : (a : I) → R) a : R)
          ((b : (a : I) → S) a : S) =
      x
⊢ Eq.{u_2 + 1} (α := S ⊗[R] S)
    (∑ x ∈ f.support,
      ∑ x_1 ∈ (a x).support,
        HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
          (b : (a : I) → S) x_1)
    (∑
      k ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((fun (i : I) ↦ ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R)) i),
      Finsupp.sum (M := R)
        ((b.repr : (a : S) → I →₀ R)
            (f.sum fun (i : I) (y : S) ↦
              HSMul.hSMul.{u_1, u_2, u_2} (α := R)
                (((fun (i : I) ↦
                          ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x) : I →₀ R))
                        i :
                      (a : I) → R)
                    k :
                  R)
                y) :
          I →₀ R)
        fun (j : I) (c : R) ↦ HSMul.hSMul (β := S ⊗[R] S) c ((b : (a : I) → S) j ⊗ₜ[R] (b : (a : I) → S) k : S ⊗[R] S))
have simp_rw : Eq.{u_2 + 1} (α := S ⊗[R] S)
  (∑ x ∈ f.support,
    ∑ x_1 ∈ (a x).support,
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((a x : (a : I) → R) x_1 : R) ((f : (a : I) → S) x : S) ⊗ₜ[R]
        (b : (a : I) → S) x_1)
  (∑ x_1 ∈ f.support,
    ∑
      x_2 ∈
        f.support.biUnion fun (i : I) ↦
          Finsupp.support.{u_4, u_1} (M := R)
            ((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)),
      HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
          ((((b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) x_1 : S) x) : I →₀ R) : (a : I) → R)
              x_2 :
            R)
          ((f : (a : I) → S) x_1 : S) ⊗ₜ[R]
        (b : (a : I) → S) x_2)
Tactic: simp_rw [map_finsuppSum, map_smul, h₁, Finsupp.sum, Finset.sum_comm (t := f.support),
    TensorProduct.smul_tmul', ← TensorProduct.sum_tmul, ← Finset.smul_sum, h₂]