-- Lean 4 proof step from Mathlib.RingTheory.PicardGroup (goal)
Goal:
R : Type u
A : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : FaithfulSMul R A
I : (Submodule R A)ˣ
T T' : Finset A
hT : (↑T : Set A) ⊆ (↑(↑I⁻¹ : Submodule R A) : Set A)
hT' : (↑T' : Set A) ⊆ (↑(↑I : Submodule R A) : Set A)
S : Finset A := Finset.image₂ (fun (x1 x2 : A) ↦ x1 * x2) T T'
r : A → R
hr : Function.support r ⊆ (↑S : Set A) ∧ Eq (α := A) (∑ a ∈ S, r a • a) 1
a : (i : ↥S) → A
ha : ∀ (i : ↥S), a i ∈ T
b : (i : ↥S) → A
hb : ∀ (i : ↥S), b i ∈ T'
eq : ∀ (i : ↥S), a i * b i = (↑i : A)
f : ↥(↑I : Submodule R A) →ₗ[R] ↥S → R :=
  LinearMap.pi (φ := fun (a : ↥S) ↦ R) fun (i : ↥S) ↦
    ((↑(LinearEquiv.symm (LinearEquiv.ofInjective (Algebra.linearMap R A) ⋯)) :
          LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) :
        LinearMap.{u, u, u_4, u} (RingHom.id R) (↥(range (Algebra.linearMap R A))) R) ∘ₗ
      (restrict (LinearMap.mulRight R (r (↑i : A) • a i)) ⋯ :
        ↥(↑I : Submodule R A) →ₗ[R] ↥(range (Algebra.linearMap R A)))
hf :
  ∀ (x : ↥(↑I : Submodule R A)) (i : ↥S),
    (algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R) = (↑x : A) * r (↑i : A) • a i
g : (↥S → R) →ₗ[R] ↥(↑I : Submodule R A) :=
  (lsum R (fun (a : ↥S) ↦ R) ℕ :
      (a : (i : ↥S) → R →ₗ[R] ↥(↑I : Submodule R A)) → ((i : ↥S) → R) →ₗ[R] ↥(↑I : Submodule R A))
    fun (i : ↥S) ↦
    toSpanSingleton R (↥(↑I : Submodule R A)) (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)
x : ↥(↑I : Submodule R A)
simp_rw :
  Eq.{u_4 + 1} (α := A)
    (∑ i : ↥S,
      (↑(HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x i : R)
            (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b i) ⋯)) :
        A))
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
simp_rw₁ :
  Eq.{u_4 + 1} (α := A)
    (∑ x_1 : ↥S, HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x x_1 : R) (b x_1))
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
simp_rw₂ :
  Eq.{u_4 + 1} (α := A)
    (∑ x_1 : ↥S,
      HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x x_1 : R) : A)
        (b x_1))
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
simp_rw₃ :
  Eq.{u_4 + 1} (α := A) (∑ x_1 : ↥S, (↑x : A) * r (↑x_1 : A) • a x_1 * b x_1)
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
⊢ Eq.{u_4 + 1} (α := A)
    (↑(∑ x_1 : ↥S,
          HSMul.hSMul.{u, u_4, u_4} (α := R) ((f : (a : ↥(↑I : Submodule R A)) → ↥S → R) x x_1 : R)
            (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑I : Submodule R A)) (b x_1) ⋯)) :
      A)
    (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
have simp_rw₄ : Eq.{u_4 + 1} (α := A) (∑ x_1 : ↥S, (↑x : A) * (r (↑x_1 : A) • a x_1 * b x_1))
  (↑((LinearMap.id : (a : ↥(↑I : Submodule R A)) → ↥(↑I : Submodule R A)) x) : A)
Tactic: simp_rw [coe_sum, coe_smul, Algebra.smul_def, hf, mul_assoc, ← Finset.mul_sum,
      Algebra.smul_mul_assoc, eq, (Finset.sum_coe_sort ..).trans hr.2, mul_one, id_apply]