-- Mathlib/LinearAlgebra/Goursat.lean
/-- **Goursat's lemma** for a submodule of a product with surjective projections.

If `L` is a submodule of `M × N` which projects fully on both factors, then there exist submodules
`M' ≤ M` and `N' ≤ N` such that `M' × N' ≤ L` and the image of `L` in `(M ⧸ M') × (N ⧸ N')` is the
graph of an isomorphism of `R`-modules `(M ⧸ M') ≃ (N ⧸ N')`.

`M` and `N` can be explicitly constructed as `L.goursatFst` and `L.goursatSnd` respectively. -/
lemma goursat_surjective : ∃ e : (M ⧸ L.goursatFst) ≃ₗ[R] N ⧸ L.goursatSnd,
    LinearMap.range ((L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ).comp L.subtype) = e.graph

Proof state:
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)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
l : M × N
hl : l ∈ L.toAddSubgroup
hl' :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨l, hl⟩ =
    (x, e x)
⊢ (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨r • l, ⋯⟩ =
    r •
      (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap
              (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
          L.toAddSubgroup.subtype)
        ⟨l, hl⟩

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3.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)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
this : ∀ (r : R) (x : M ⧸ L.goursatFst), e (r • x) = r • e x
e_1✝ :
  AddSubgroup ((M ⧸ L.goursatFst) × N ⧸ L.goursatSnd) =
    AddSubgroup ((M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
⊢ (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯,
            right_inv := ⋯ }).graph.toAddSubgroup =
    e.toAddMonoidHom.graph

Tactic:
ext v

Result:
case h.e'_3.h.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)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
this : ∀ (r : R) (x : M ⧸ L.goursatFst), e (r • x) = r • e x
e_1✝ :
  AddSubgroup ((M ⧸ L.goursatFst) × N ⧸ L.goursatSnd) =
    AddSubgroup ((M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
v : (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd
⊢ v ∈
      (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯,
              right_inv := ⋯ }).graph.toAddSubgroup ↔
    v ∈ e.toAddMonoidHom.graph

Proof state:
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)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
this :
  ∃ x_1,
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
          L.toAddSubgroup.subtype)
        x_1 =
      (x, e x)
⊢ r • (x, e x) ∈
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range

Tactic:
rcases this with ⟨⟨l, hl⟩, hl'⟩

Result:
case intro.mk
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)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
l : M × N
hl : l ∈ L.toAddSubgroup
hl' :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype)
      ⟨l, hl⟩ =
    (x, e x)
⊢ r • (x, e x) ∈
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range

Proof state:
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)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
this : (x, e x) ∈ e.toAddMonoidHom.graph
⊢ r • (x, e x) ∈
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range

Tactic:
rw [← he, AddMonoidHom.mem_range] at this

Result:
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)
hL₁ : Surjective (Prod.fst ∘ ⇑L.subtype)
hL₂ : Surjective (Prod.snd ∘ ⇑L.subtype)
e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd
he :
  (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range =
    e.toAddMonoidHom.graph
r : R
x : M ⧸ L.goursatFst
this :
  ∃ x_1,
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
          L.toAddSubgroup.subtype)
        x_1 =
      (x, e x)
⊢ r • (x, e x) ∈
    (((QuotientAddGroup.mk' L.toAddSubgroup.goursatFst).prodMap (QuotientAddGroup.mk' L.toAddSubgroup.goursatSnd)).comp
        L.toAddSubgroup.subtype).range