-- Lean 4 proof step from Mathlib.LinearAlgebra.Span.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Type u_8
inst_3 : AddCommMonoid N
inst_4 : Module R N
S : Set M
f g : LinearMap.{u_1, u_1, u_4, u_8} (RingHom.id R) (↥(span R S)) N
h :
  ∀ (s : (↑S : Type u_4)),
    Eq.{u_8 + 1} (α := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) (↑s : M) ⋯) :
        N)
x_1 x y : M
hx : Membership.mem (γ := Submodule R M) (span R S) x
hy : Membership.mem (γ := Submodule R M) (span R S) y
hx' :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
hy' :
  Eq.{u_8 + 1} (α := N)
    ((f : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
mpr :
  HAdd.hAdd (α := N) (β := N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
        N) =
    HAdd.hAdd (α := N) (β := N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
        N)
⊢ HAdd.hAdd (α := N) (β := N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((f : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
        N) =
    HAdd.hAdd (α := N) (β := N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
        N)
      ((g : (a : ↥(span R S)) → N)
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
        N)
have mpr₁ : HAdd.hAdd (α := N) (β := N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N) =
  HAdd.hAdd (α := N) (β := N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) x hx) :
      N)
    ((g : (a : ↥(span R S)) → N)
        (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R S) x) y hy) :
      N)
Tactic: rw [hx', hy']