-- 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
⊢ 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)))
have h : 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)))))) =
  (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
Tactic: convert! goursatFst_prod_goursatSnd_le (range <| P.prod Q)