awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)))
⊢ 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
have 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' := sorry, map_smul' := this, invFun := e.invFun, left_inv := sorry, right_inv := sorry :
                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: ext v
-- 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)
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)
⊢ 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
have h : (((↑{ toFun := e.toFun, map_add' := sorry, map_smul' := this, invFun := e.invFun, left_inv := sorry, right_inv := sorry } :
            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: rw [mem_toAddSubgroup, mem_graph_iff, Eq.comm]
-- 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
⊢ Surjective (α := ↥L') (β := ↥M')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.fst (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
have simp : map (LinearMap.fst R ↥M' ↥N') L' = ⊤
Tactic: simp only [← coe_fst (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Goursat (hypothesis)
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
⊢ ∃ (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)
have hL₁' : 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
-- 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'))
⊢ Surjective (α := ↥L') (β := ↥N')
    (Function.comp (β := Prod.{u_2, u_3} ↥M' ↥N') Prod.snd (⇑L'.subtype : (a : ↥L') → ↥M' × ↥N'))
have simp : map (LinearMap.snd R ↥M' ↥N') L' = ⊤
Tactic: simp only [← coe_snd (R := R), ← coe_comp, ← range_eq_top, LinearMap.range_comp, range_subtype]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Goursat (hypothesis)
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'))
⊢ ∃ (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)
have hL₂' : 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
-- 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'))
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨e, he⟩ := goursat_surjective hL₁' hL₂'
-- 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
⊢ ∃ (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)
have 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)
Tactic: use M', N', L'.goursatFst, L'.goursatSnd, e
-- 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
⊢ L =
    map (M'.subtype.prodMap N'.subtype)
      (comap (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ) (↑e : ↥M' ⧸ L'.goursatFst →ₗ[R] ↥N' ⧸ L'.goursatSnd).graph)
have 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)
Tactic: rw [← he]
-- 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
⊢ 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)
have h : L =
  map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
    (comap (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))))))
      (map
        (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)))))
Tactic: simp only [LinearMap.range_comp, Submodule.range_subtype, L', M', N', P, Q]
-- 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
⊢ L =
    map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
      (comap (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))))))
        (map
          (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 : 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: rw [comap_map_eq_self]
-- 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
⊢ 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)))
have 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)))
Tactic: ext ⟨m, n⟩
-- 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
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)))
have h : (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)))
Tactic: constructor