Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : 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' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ L =
    map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
      (comap
        ((((LinearMap.fst R M N).submoduleMap L).prod
                    ((LinearMap.snd R M N).submoduleMap L)).range.goursatFst.mkQ.prodMap
          (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatSnd.mkQ)
        (map
          ((((LinearMap.fst R M N).submoduleMap L).prod
                      ((LinearMap.snd R M N).submoduleMap L)).range.goursatFst.mkQ.prodMap
            (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatSnd.mkQ)
          (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range))

Tactic:
comap_map_eq_self

Goal state after:
case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : 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' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ L =
    map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
      (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range

case h
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : 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' := (LinearMap.fst R M N).submoduleMap L
Q : ↥L →ₗ[R] ↥N' := (LinearMap.snd R M N).submoduleMap L
L' : Submodule R (↥M' × ↥N') := (P.prod Q).range
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
⊢ ((((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatFst.mkQ.prodMap
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range.goursatSnd.mkQ).ker ≤
    (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range