-- 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)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
P : ↥L →ₗ[R] ↥M' := submoduleMap (LinearMap.fst R M N) L
Q : ↥L →ₗ[R] ↥N' := submoduleMap (LinearMap.snd R M N) L
L' : Submodule R (Prod.{u_2, u_3} ↥M' ↥N') := (P.prod Q).range
hL₁' :
  Surjective (α := ↥L') (β := ↥M')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.fst (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
hL₂' :
  Surjective (α := ↥L') (β := ↥N')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.snd (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥M' ⧸ L'.goursatFst) (↥N' ⧸ L'.goursatSnd)
he :
  (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range =
    (↑e : ↥M' ⧸ L'.goursatFst →ₗ[R] ↥N' ⧸ L'.goursatSnd).graph
h :
  L =
    map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
      (LinearMap.range (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))
⊢ L =
    map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
      (comap (M₂ :=
        Prod.{u_2, u_3}
          (HasQuotient.Quotient ↥(map (LinearMap.fst R M N) L) (B := Submodule R ↥(map (LinearMap.fst R M N) L))
            (goursatFst (N := ↥(map (LinearMap.snd R M N) L))
              (LinearMap.range
                (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
          (HasQuotient.Quotient ↥(map (LinearMap.snd R M N) L) (B := Submodule R ↥(map (LinearMap.snd R M N) L))
            (goursatSnd (M := ↥(map (LinearMap.fst R M N) L))
              (LinearMap.range
                (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L))))))
        (prodMap
          (mkQ
            (goursatFst (N := ↥(map (LinearMap.snd R M N) L))
              (LinearMap.range
                (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
          (mkQ
            (goursatSnd (M := ↥(map (LinearMap.fst R M N) L))
              (LinearMap.range
                (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L))))))
        (map
          (prodMap
            (mkQ
              (goursatFst (N := ↥(map (LinearMap.snd R M N) L))
                (LinearMap.range
                  (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
            (mkQ
              (goursatSnd (M := ↥(map (LinearMap.fst R M N) L))
                (LinearMap.range
                  (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L))))))
          (LinearMap.range
            (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
have h₁ : LE.le (α := Submodule R (Prod.{u_2, u_3} ↥(map (LinearMap.fst R M N) L) ↥(map (LinearMap.snd R M N) L)))
  (ker (M₂ :=
    Prod.{u_2, u_3}
      (HasQuotient.Quotient ↥(map (LinearMap.fst R M N) L) (B := Submodule R ↥(map (LinearMap.fst R M N) L))
        (goursatFst (N := ↥(map (LinearMap.snd R M N) L))
          (LinearMap.range
            (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
      (HasQuotient.Quotient ↥(map (LinearMap.snd R M N) L) (B := Submodule R ↥(map (LinearMap.snd R M N) L))
        (goursatSnd (M := ↥(map (LinearMap.fst R M N) L))
          (LinearMap.range
            (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L))))))
    (prodMap
      (mkQ
        (goursatFst (N := ↥(map (LinearMap.snd R M N) L))
          (LinearMap.range
            (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))
      (mkQ
        (goursatSnd (M := ↥(map (LinearMap.fst R M N) L))
          (LinearMap.range
            (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))))))
  (LinearMap.range (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))
Tactic: rw [comap_map_eq_self]