-- Lean 4 proof step from Mathlib.LinearAlgebra.Goursat (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
L : Submodule R (M × N)
hL₁ : Surjective (α := ↥L) (β := M) (Function.comp (β := M × N) Prod.fst (⇑L.subtype : (a : ↥L) → M × N))
hL₂ : Surjective (α := ↥L) (β := N) (Function.comp (β := M × N) Prod.snd (⇑L.subtype : (a : ↥L) → M × N))
e : AddEquiv.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
he :
  AddMonoidHom.range (G := ↥(L.toAddSubgroup : AddSubgroup (M × N)))
      (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup)) =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
l : M × N
hl : Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) l
hl' :
  Eq (α := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
    ((AddMonoidHom.comp
            (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
              (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
            (AddSubgroup.subtype L.toAddSubgroup) :
          (a : ↥L.toAddSubgroup) → (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd)
        (Subtype.mk (p := fun (x : M × N) ↦
          Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) l hl) :
      Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
    ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
⊢ (AddMonoidHom.comp
          (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
            (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
          (AddSubgroup.subtype L.toAddSubgroup) :
        (a : ↥L.toAddSubgroup) → (M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
      (Subtype.mk (p := fun (x : M × N) ↦
        Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) (r • l) ⋯) =
    HSMul.hSMul (β := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) r
      ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
have h : (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup) :
      (a : ↥L.toAddSubgroup) → (M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
    (Subtype.mk (p := fun (x : M × N) ↦
      Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) (r • l) sorry) =
  HSMul.hSMul (β := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) r
    ((AddMonoidHom.comp
            (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
              (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
            (AddSubgroup.subtype L.toAddSubgroup) :
          (a : ↥L.toAddSubgroup) → (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd)
        (Subtype.mk (p := fun (x : M × N) ↦
          Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) l hl) :
      Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
Tactic: rw [← hl']