-- 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
this :
  ∃ (x_1 : ↥(L.toAddSubgroup : AddSubgroup (M × N))),
    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)
          x_1 :
        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))
⊢ Membership.mem (γ := AddSubgroup (Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)))
    (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)))
    (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 rcases : ∀ (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))),
  Membership.mem (γ := AddSubgroup (Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)))
    (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)))
    (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)))
Tactic: rcases this with ⟨⟨l, hl⟩, hl'⟩
Cleared hypotheses: this