awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Goursat
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)
hL₁ : Surjective (α := ↥L) (β := M) (Function.comp (β := M × N) Prod.fst (⇑L.subtype : (a : ↥L) → M × N))
hL₂ : Surjective (α := ↥L) (β := N) (Function.comp (β := M × N) Prod.snd (⇑L.subtype : (a : ↥L) → M × N))
e : AddEquiv.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
he :
  AddMonoidHom.range (G := ↥(L.toAddSubgroup : AddSubgroup (M × N)))
      (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup)) =
    e.toAddMonoidHom.graph
this :
  ∀ (r : R) (x : M ⧸ L.goursatFst),
    (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) (r • x) =
      HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)
h :
  (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range.toAddSubgroup =
    toAddSubgroup (module_M := Prod.instModule)
      (graph
        (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } :
          M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd))
⊢ (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range =
    graph
      (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } :
        M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd)

Tactic:
rw [← toAddSubgroup_injective.eq_iff]

Premises used: Function.Injective.eq_iff, Submodule.toAddSubgroup_injective
-- Module: Mathlib.LinearAlgebra.Goursat
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)
hL₁ : Surjective (α := ↥L) (β := M) (Function.comp (β := M × N) Prod.fst (⇑L.subtype : (a : ↥L) → M × N))
hL₂ : Surjective (α := ↥L) (β := N) (Function.comp (β := M × N) Prod.snd (⇑L.subtype : (a : ↥L) → M × N))
e : AddEquiv.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
he :
  AddMonoidHom.range (G := ↥(L.toAddSubgroup : AddSubgroup (M × N)))
      (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup)) =
    e.toAddMonoidHom.graph
this :
  ∀ (r : R) (x : M ⧸ L.goursatFst),
    (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) (r • x) =
      HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)
⊢ AddMonoidHom.range (G := ↥(L.toAddSubgroup : AddSubgroup (M × N)))
      (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup)) =
    e.toAddMonoidHom.graph

Tactic:
he
-- Module: Mathlib.LinearAlgebra.Goursat
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)
hL₁ : Surjective (α := ↥L) (β := M) (Function.comp (β := M × N) Prod.fst (⇑L.subtype : (a : ↥L) → M × N))
hL₂ : Surjective (α := ↥L) (β := N) (Function.comp (β := M × N) Prod.snd (⇑L.subtype : (a : ↥L) → M × N))
e : AddEquiv.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
he :
  AddMonoidHom.range (G := ↥(L.toAddSubgroup : AddSubgroup (M × N)))
      (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup)) =
    e.toAddMonoidHom.graph
this :
  ∀ (r : R) (x : M ⧸ L.goursatFst),
    (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) (r • x) =
      HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)
h :
  AddSubgroup (Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) =
      AddSubgroup
        (Prod.{u_2, u_3}
          (HasQuotient.Quotient M (B := AddSubgroup M) (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (HasQuotient.Quotient N (B := AddSubgroup N) (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup))) →
    toAddSubgroup (module_M := Prod.instModule)
        (graph
          (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ :
                LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd) } :
            M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd)) =
      e.toAddMonoidHom.graph
⊢ (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range.toAddSubgroup =
    toAddSubgroup (module_M := Prod.instModule)
      (graph
        (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } :
          M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd))

Tactic:
convert! he using 1
-- Module: Mathlib.LinearAlgebra.Goursat
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)
hL₁ : Surjective (α := ↥L) (β := M) (Function.comp (β := M × N) Prod.fst (⇑L.subtype : (a : ↥L) → M × N))
hL₂ : Surjective (α := ↥L) (β := N) (Function.comp (β := M × N) Prod.snd (⇑L.subtype : (a : ↥L) → M × N))
e : AddEquiv.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
he :
  AddMonoidHom.range (G := ↥(L.toAddSubgroup : AddSubgroup (M × N)))
      (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup)) =
    e.toAddMonoidHom.graph
this :
  ∀ (r : R) (x : M ⧸ L.goursatFst),
    (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) (r • x) =
      HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)
e_1 :
  AddSubgroup (Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) =
    AddSubgroup
      (Prod.{u_2, u_3}
        (HasQuotient.Quotient M (B := AddSubgroup M) (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
        (HasQuotient.Quotient N (B := AddSubgroup N) (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
h :
  ∀ (v : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)),
    v ∈
        toAddSubgroup (module_M := Prod.instModule)
          (graph
            (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ :
                  LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd) } :
              M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd)) ↔
      v ∈ e.toAddMonoidHom.graph
⊢ toAddSubgroup (module_M := Prod.instModule)
      (graph
        (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ :
              LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd) } :
          M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd)) =
    e.toAddMonoidHom.graph

Tactic:
ext v
-- Module: Mathlib.LinearAlgebra.Goursat
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)
hL₁ : Surjective (α := ↥L) (β := M) (Function.comp (β := M × N) Prod.fst (⇑L.subtype : (a : ↥L) → M × N))
hL₂ : Surjective (α := ↥L) (β := N) (Function.comp (β := M × N) Prod.snd (⇑L.subtype : (a : ↥L) → M × N))
e : AddEquiv.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
he :
  AddMonoidHom.range (G := ↥(L.toAddSubgroup : AddSubgroup (M × N)))
      (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup)) =
    e.toAddMonoidHom.graph
this :
  ∀ (r : R) (x : M ⧸ L.goursatFst),
    (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) (r • x) =
      HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)
e_1 :
  AddSubgroup (Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) =
    AddSubgroup
      (Prod.{u_2, u_3}
        (HasQuotient.Quotient M (B := AddSubgroup M) (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
        (HasQuotient.Quotient N (B := AddSubgroup N) (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
v : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
h :
  (((↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } :
              LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) :
          (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd)
        v.1 =
      v.2 ↔
    v ∈ e.toAddMonoidHom.graph
⊢ v ∈
      toAddSubgroup (module_M := Prod.instModule)
        (graph
          (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ :
                LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd) } :
            M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd)) ↔
    v ∈ e.toAddMonoidHom.graph

Tactic:
rw [mem_toAddSubgroup, mem_graph_iff, Eq.comm]

Premises used: Submodule.mem_toAddSubgroup, Eq.comm, LinearMap.mem_graph_iff
-- Module: Mathlib.LinearAlgebra.Goursat
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)
hL₁ : Surjective (α := ↥L) (β := M) (Function.comp (β := M × N) Prod.fst (⇑L.subtype : (a : ↥L) → M × N))
hL₂ : Surjective (α := ↥L) (β := N) (Function.comp (β := M × N) Prod.snd (⇑L.subtype : (a : ↥L) → M × N))
e : AddEquiv.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
he :
  AddMonoidHom.range (G := ↥(L.toAddSubgroup : AddSubgroup (M × N)))
      (AddMonoidHom.comp
        (AddMonoidHom.prodMap (QuotientAddGroup.mk' (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
          (QuotientAddGroup.mk' (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
        (AddSubgroup.subtype L.toAddSubgroup)) =
    e.toAddMonoidHom.graph
this :
  ∀ (r : R) (x : M ⧸ L.goursatFst),
    (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) (r • x) =
      HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)
e_1 :
  AddSubgroup (Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) =
    AddSubgroup
      (Prod.{u_2, u_3}
        (HasQuotient.Quotient M (B := AddSubgroup M) (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup))
        (HasQuotient.Quotient N (B := AddSubgroup N) (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup)))
v : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)
⊢ (((↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } :
              LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) :
            LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) :
          (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd)
        v.1 =
      v.2 ↔
    v ∈ e.toAddMonoidHom.graph

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Goursat
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
simp : map (LinearMap.fst R ↥M' ↥N') L' = ⊤
⊢ Surjective (α := ↥L') (β := ↥M')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.fst (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))

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

Premises used: LinearMap.range_comp, LinearMap.coe_fst, LinearMap.range_eq_top, LinearMap.coe_comp, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.Goursat
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
⊢ map (LinearMap.fst R ↥M' ↥N') L' = ⊤

Tactic:
simpa only [L', ← LinearMap.range_comp, fst_prod, range_eq_top] using
      (LinearMap.fst ..).submoduleMap_surjective L

Premises used: LinearMap.fst, LinearMap.fst_prod, LinearMap.range_comp, LinearMap.range_eq_top, LinearMap.submoduleMap_surjective
-- Module: Mathlib.LinearAlgebra.Goursat
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
⊢ Surjective (α := ↥L') (β := ↥M')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.fst (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))

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
-- Module: Mathlib.LinearAlgebra.Goursat
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'))
simp : map (LinearMap.snd R ↥M' ↥N') L' = ⊤
⊢ Surjective (α := ↥L') (β := ↥N')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.snd (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))

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

Premises used: LinearMap.range_comp, LinearMap.range_eq_top, LinearMap.coe_snd, LinearMap.coe_comp, Submodule.range_subtype
-- Module: Mathlib.LinearAlgebra.Goursat
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'))
⊢ map (LinearMap.snd R ↥M' ↥N') L' = ⊤

Tactic:
simpa only [L', ← LinearMap.range_comp, snd_prod, range_eq_top] using
      (LinearMap.snd ..).submoduleMap_surjective L

Premises used: LinearMap.snd, LinearMap.range_comp, LinearMap.range_eq_top, LinearMap.snd_prod, LinearMap.submoduleMap_surjective
-- Module: Mathlib.LinearAlgebra.Goursat
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'))
⊢ Surjective (α := ↥L') (β := ↥N')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.snd (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))

Tactic:
have hL₂' : Surjective (Prod.snd ∘ L'.subtype) := by
    simp only [← coe_snd (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
    simpa only [L', ← LinearMap.range_comp, snd_prod, range_eq_top] using
      (LinearMap.snd ..).submoduleMap_surjective L
-- Module: Mathlib.LinearAlgebra.Goursat
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'))
obtain :
  ∀ (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),
    ∃ (M' : Submodule R M) (N' : Submodule R N) (M'' : Submodule R ↥M') (N'' : Submodule R ↥N') (e :
      LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥M' ⧸ M'') (↥N' ⧸ N'')),
      L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e : ↥M' ⧸ M'' →ₗ[R] ↥N' ⧸ N'').graph)
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N) (M'' : Submodule R ↥M') (N'' : Submodule R ↥N') (e :
    LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥M' ⧸ M'') (↥N' ⧸ N'')),
    L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e : ↥M' ⧸ M'' →ₗ[R] ↥N' ⧸ N'').graph)

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

Premises used: Submodule.goursat_surjective
-- Module: Mathlib.LinearAlgebra.Goursat
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 (M'.subtype.prodMap N'.subtype)
      (comap (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ) (↑e : ↥M' ⧸ L'.goursatFst →ₗ[R] ↥N' ⧸ L'.goursatSnd).graph)
⊢ ∃ (M' : Submodule R M) (N' : Submodule R N) (M'' : Submodule R ↥M') (N'' : Submodule R ↥N') (e :
    LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥M' ⧸ M'') (↥N' ⧸ N'')),
    L = map (M'.subtype.prodMap N'.subtype) (comap (M''.mkQ.prodMap N''.mkQ) (↑e : ↥M' ⧸ M'' →ₗ[R] ↥N' ⧸ N'').graph)

Tactic:
use M', N', L'.goursatFst, L'.goursatSnd, e

Premises used: Submodule.goursatSnd, Submodule.goursatFst
-- Module: Mathlib.LinearAlgebra.Goursat
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 (M'.subtype.prodMap N'.subtype)
      (comap (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ)
        (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range)
⊢ L =
    map (M'.subtype.prodMap N'.subtype)
      (comap (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ) (↑e : ↥M' ⧸ L'.goursatFst →ₗ[R] ↥N' ⧸ L'.goursatSnd).graph)

Tactic:
rw [← he]
-- Module: Mathlib.LinearAlgebra.Goursat
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 :
  ∀ (m : M) (n : N),
    (m, n) ∈ L ↔
      (m, n) ∈
        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)
      (LinearMap.range (LinearMap.prod (submoduleMap (LinearMap.fst R M N) L) (submoduleMap (LinearMap.snd R M N) L)))

Tactic:
ext ⟨m, n⟩