awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : GeneralLinearGroup R M
x : M
⊢ Eq (α := M)
    (((↑((generalLinearEquiv R M : (a : GeneralLinearGroup R M) → M ≃ₗ[R] M) f) : M →ₗ[R] M) : (a : M) → M) x : M)
    (((↑f : M →ₗ[R] M) : (a : M) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
f : GeneralLinearGroup R M
⊢ Eq (α := (a : M) → M)
    (⇑((generalLinearEquiv R M : (a : GeneralLinearGroup R M) → M ≃ₗ[R] M) f : M ≃ₗ[R] M) : (a : M) → M)
    (⇑(↑f : M →ₗ[R] M) : (a : M) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R₁ : Type u_3
R₂ : Type u_4
M₁ : Type u_6
M₂ : Type u_7
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M₁
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
g : GeneralLinearGroup R₁ M₁
⊢ (congrLinearEquiv e₁₂ : (a : GeneralLinearGroup R₁ M₁) → GeneralLinearGroup R₂ M₂) g =
    ofLinearEquiv (e₁₂.symm.trans (re₂₃ := inst_6) (re₃₂ := inst_7) (g.toLinearEquiv.trans e₁₂))

Tactic:
rfl

Premises used: LinearMap.GeneralLinearGroup.ofLinearEquiv, rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R₁ : Type u_3
R₂ : Type u_4
M₁ : Type u_6
M₂ : Type u_7
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : Module R₁ M₁
inst_5 : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_6 : RingHomInvPair σ₁₂ σ₂₁
inst_7 : RingHomInvPair σ₂₁ σ₁₂
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ (congrLinearEquiv e₁₂).symm = congrLinearEquiv e₁₂.symm

Tactic:
rfl

Premises used: Units.mapEquiv, Equiv.symm, MulEquiv.symm, LinearMap.GeneralLinearGroup.congrLinearEquiv, rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R : Type u_1
inst : Semiring R
N₁ : Type u_9
N₂ : Type u_10
N₃ : Type u_11
inst_1 : AddCommMonoid N₁
inst_2 : AddCommMonoid N₂
inst_3 : AddCommMonoid N₃
inst_4 : Module R N₁
inst_5 : Module R N₂
inst_6 : Module R N₃
e₁₂ : N₁ ≃ₗ[R] N₂
e₂₃ : N₂ ≃ₗ[R] N₃
⊢ (congrLinearEquiv e₁₂).trans (congrLinearEquiv e₂₃) = congrLinearEquiv (e₁₂ ≪≫ₗ e₂₃)

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.trans, Units.mapEquiv, LinearMap.GeneralLinearGroup.congrLinearEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R₁ : Type u_3
R₂ : Type u_4
R₃ : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
inst_3 : AddCommMonoid M₁
inst_4 : AddCommMonoid M₂
inst_5 : AddCommMonoid M₃
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
σ₂₁ : R₂ →+* R₁
σ₃₂ : R₃ →+* R₂
σ₃₁ : R₃ →+* R₁
inst_9 : RingHomInvPair σ₁₂ σ₂₁
inst_10 : RingHomInvPair σ₂₃ σ₃₂
inst_11 : RingHomInvPair σ₁₃ σ₃₁
inst_12 : RingHomInvPair σ₂₁ σ₁₂
inst_13 : RingHomInvPair σ₃₂ σ₂₃
inst_14 : RingHomInvPair σ₃₁ σ₁₃
inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst_16 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃
⊢ (congrLinearEquiv e₁₂).trans (congrLinearEquiv e₂₃) = congrLinearEquiv (e₁₂.trans e₂₃)

Tactic:
rfl

Premises used: Equiv.trans, MulEquiv.trans, Units.mapEquiv, LinearMap.GeneralLinearGroup.congrLinearEquiv, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
Goal:
R₁ : Type u_3
M₁ : Type u_6
inst : Semiring R₁
inst_1 : AddCommMonoid M₁
inst_2 : Module R₁ M₁
⊢ Eq (α := GeneralLinearGroup R₁ M₁ ≃* GeneralLinearGroup R₁ M₁) (congrLinearEquiv (LinearEquiv.refl R₁ M₁))
    (MulEquiv.refl (GeneralLinearGroup R₁ M₁))

Tactic:
rfl

Premises used: MulEquiv.refl, Units.mapEquiv, Equiv.refl, LinearMap.GeneralLinearGroup.congrLinearEquiv, 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)
h :
  ∀ (x : M),
    x ∈ L.goursatFst.toAddSubgroup ↔
      Membership.mem (γ := AddSubgroup M) (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup) x
⊢ L.goursatFst.toAddSubgroup = AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup

Tactic:
ext x
-- 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)
x : M
⊢ x ∈ L.goursatFst.toAddSubgroup ↔
    Membership.mem (γ := AddSubgroup M) (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup) x

Tactic:
simp [goursatFst, AddSubgroup.mem_goursatFst]

Premises used: AddSubgroup.mem_goursatFst, 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)
h :
  ∀ (x : N),
    x ∈ L.goursatSnd.toAddSubgroup ↔
      Membership.mem (γ := AddSubgroup N) (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup) x
⊢ L.goursatSnd.toAddSubgroup = AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup

Tactic:
ext x
-- 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)
x : N
⊢ x ∈ L.goursatSnd.toAddSubgroup ↔
    Membership.mem (γ := AddSubgroup N) (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup) x

Tactic:
simp [goursatSnd, AddSubgroup.mem_goursatSnd]

Premises used: Submodule.goursatSnd, AddSubgroup.mem_goursatSnd
-- 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)
⊢ L.goursatFst.prod L.goursatSnd ≤ L

Tactic:
simpa only [← toAddSubgroup_le, goursatFst_toAddSubgroup, goursatSnd_toAddSubgroup]
    using L.toAddSubgroup.goursatFst_prod_goursatSnd_le

Premises used: Submodule.goursatSnd_toAddSubgroup, Submodule.toAddSubgroup, Submodule.goursatFst_toAddSubgroup, AddSubgroup.goursatFst_prod_goursatSnd_le, Submodule.toAddSubgroup_le
-- 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))
obtain :
  ∀ (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),
    ∃ (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)),
      (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range =
        (↑e : M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd).graph
⊢ ∃ (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)),
    (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range =
      (↑e : M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd).graph

Tactic:
obtain ⟨(e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd), he⟩ :=
    L.toAddSubgroup.goursat_surjective hL₁ hL₂

Premises used: Submodule.goursatSnd, AddSubgroup.goursat_surjective, 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)
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
r : R
x : M ⧸ L.goursatFst
change :
  (r • x,
      HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)) ∈
    e.toAddMonoidHom.graph
⊢ (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)

Tactic:
change (r • x, r • e x) ∈ e.toAddMonoidHom.graph

Premises used: AddEquiv.toAddMonoidHom, Prod.mk, AddMonoidHom.graph, HSMul.hSMul, DFunLike.coe
-- 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
r : R
x : M ⧸ L.goursatFst
rw :
  Membership.mem (γ := AddSubgroup (Prod.{u_2, u_3} (M ⧸ L.goursatFst) (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)))
    (HSMul.hSMul (β := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) r
      ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (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.toAddMonoidHom.graph

Tactic:
rw [← he, ← Prod.smul_mk]

Premises used: Prod.smul_mk
-- 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
r : R
x : M ⧸ L.goursatFst
⊢ Membership.mem (α := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) e.toAddMonoidHom.graph
    ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))

Tactic:
have : (x, e x) ∈ e.toAddMonoidHom.graph := 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)
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
r : R
x : M ⧸ L.goursatFst
this :
  Membership.mem (α := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) e.toAddMonoidHom.graph
    ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
⊢ ∃ (x_1 : ↥(L.toAddSubgroup : AddSubgroup (M × N))),
    Eq (α := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
      ((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) :
            (a : ↥L.toAddSubgroup) → (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd)
          x_1 :
        Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
      ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))

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

Premises used: AddMonoidHom.mem_range
-- 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
r : R
x : M ⧸ L.goursatFst
l : M × N
hl : Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) l
hl' :
  Eq (α := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
    ((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) :
          (a : ↥L.toAddSubgroup) → (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd)
        (Subtype.mk (p := fun (x : M × N) ↦
          Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) l hl) :
      Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
    ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
h :
  (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) :
        (a : ↥L.toAddSubgroup) → (M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
      (Subtype.mk (p := fun (x : M × N) ↦
        Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) (r • l) ⋯) =
    HSMul.hSMul (β := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) r
      ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
⊢ Membership.mem (γ := AddSubgroup (Prod.{u_2, u_3} (M ⧸ L.goursatFst) (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)))
    (HSMul.hSMul (β := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) r
      ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)))

Tactic:
use ⟨r • l, L.smul_mem r hl⟩
-- 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
r : R
x : M ⧸ L.goursatFst
l : M × N
hl : Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) l
hl' :
  Eq (α := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
    ((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) :
          (a : ↥L.toAddSubgroup) → (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd)
        (Subtype.mk (p := fun (x : M × N) ↦
          Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) l hl) :
      Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
    ((x, (e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x) : Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))
⊢ (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) :
        (a : ↥L.toAddSubgroup) → (M ⧸ L.toAddSubgroup.goursatFst) × N ⧸ L.toAddSubgroup.goursatSnd)
      (Subtype.mk (p := fun (x : M × N) ↦
        Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) (r • l) ⋯) =
    HSMul.hSMul (β := Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)) r
      ((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) :
            (a : ↥L.toAddSubgroup) → (M ⧸ L.goursatFst) × N ⧸ L.goursatSnd)
          (Subtype.mk (p := fun (x : M × N) ↦
            Membership.mem (γ := AddSubgroup (M × N)) (L.toAddSubgroup : AddSubgroup (M × N)) x) l hl) :
        Prod.{u_2, u_3} (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd))

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)
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
⊢ ∀ (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)

Tactic:
have (r : R) (x : M ⧸ L.goursatFst) : e (r • x) = r • e x := by
    change (r • x, r • e x) ∈ e.toAddMonoidHom.graph
    rw [← he, ← Prod.smul_mk]
    have : (x, e x) ∈ e.toAddMonoidHom.graph := rfl
    rw [← he, AddMonoidHom.mem_range] at this
    rcases this with ⟨⟨l, hl⟩, hl'⟩
    use ⟨r • l, L.smul_mem r hl⟩
    rw [← hl']
    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)
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 =
    graph
      (↑{ toFun := e.toFun, map_add' := ⋯, map_smul' := this, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯ } :
        M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd)
⊢ ∃ (e : LinearEquiv.{u_1, u_1, u_2, u_3} (RingHom.id R) (M ⧸ L.goursatFst) (N ⧸ L.goursatSnd)),
    (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range =
      (↑e : M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd).graph

Tactic:
use { e with map_smul' := this }