-- Mathlib/LinearAlgebra/Goursat.lean
/-- **Goursat's lemma** for an arbitrary submodule of a product.

If `L` is a submodule of `M × N`, then there exist submodules `M'' ≤ M' ≤ M` and `N'' ≤ N' ≤ N` such
that `L ≤ M' × N'`, and `L` is (the image in `M × N` of) the preimage of the graph of an `R`-linear
isomorphism `M' ⧸ M'' ≃ N' ⧸ N''`. -/
lemma goursat : ∃ (M' : Submodule R M) (N' : Submodule R N) (M'' : Submodule R M')
    (N'' : Submodule R N') (e : (M' ⧸ M'') ≃ₗ[R] N' ⧸ N''),
    L = (e.graph.comap <| M''.mkQ.prodMap N''.mkQ).map (M'.subtype.prodMap N'.subtype)

Proof state:
case h.h.mk.mp
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') := LinearMap.range (P.prod Q)
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : LinearMap.range (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype) = (↑e).graph
m : M
n : N
hmn : (m, n) ∈ L
⊢ ∃ (x : ∃ x, (m, x) ∈ L) (x_1 : ∃ a, (a, n) ∈ L),
    ∃ a b, ∃ (b_1 : (a, b) ∈ L), Pi.prod ⇑P ⇑Q ⟨(a, b), b_1⟩ = (⟨m, ⋯⟩, ⟨n, ⋯⟩)

Tactic:
exact ⟨⟨n, hmn⟩, ⟨m, hmn⟩, ⟨m, n, hmn, rfl⟩⟩

Result:
no goals

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)
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') := LinearMap.range (P.prod Q)
⊢ ∃ M' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)

Tactic:
have hL₁' : Surjective (Prod.fst ∘ L'.subtype) := by
  simp only [← coe_fst (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
  simpa only [L', ← LinearMap.range_comp, fst_prod, range_eq_top] using
    (LinearMap.fst ..).submoduleMap_surjective L

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)
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') := LinearMap.range (P.prod Q)
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
⊢ ∃ M' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).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)
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') := LinearMap.range (P.prod Q)
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
⊢ ∃ M' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)

Tactic:
obtain ⟨e, he⟩ := goursat_surjective hL₁' hL₂'

Result:
case intro
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') := LinearMap.range (P.prod Q)
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : LinearMap.range (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype) = (↑e).graph
⊢ ∃ M' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).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)
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') := LinearMap.range (P.prod Q)
⊢ Surjective (Prod.fst ∘ ⇑L'.subtype)

Tactic:
simp only [← coe_fst (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]

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)
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') := LinearMap.range (P.prod Q)
⊢ map (LinearMap.fst R ↥M' ↥N') L' = ⊤

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)
M' : Submodule R M := map (LinearMap.fst R M N) L
⊢ ∃ M' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)

Tactic:
let N' := L.map (LinearMap.snd ..)

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)
M' : Submodule R M := map (LinearMap.fst R M N) L
N' : Submodule R N := map (LinearMap.snd R M N) L
⊢ ∃ M' N' M'' N'' e, L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e).graph)