awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (hypothesis)
Goal:
K : Type u_1
V : Type u_2
W : Type u_3
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
inst_4 : AddCommMonoid W
inst_5 : Module K W
inst_6 : Projective K W
f : AlgEquiv.{u_1, u_2, u_3} K (End K V) (End K W)
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : Ne.{u_1 + 1} (α := K) ((v : (a : V) → K) u : K) (0 : K)
z : W
hz :
  ¬Eq (α := W) ((((f : (a : End K V) → End K W) (smulRight v u) : End K W) : (a : W) → W) z : W)
      ((0 : (a : W) → W) z : W)
T : V →ₗ[K] W :=
  (applyₗ : (a : W) → (W →ₗ[K] W) →ₗ[K] W) z ∘ₗ f.toLinearMap ∘ₗ (smulRightₗ : (a : V →ₗ[K] K) → V →ₗ[K] V →ₗ[K] V) v
hT :
  ∀ (x : V),
    Eq.{u_3 + 1} (α := W) ((T : (a : V) → W) x : W)
      ((((f : (a : End K V) → End K W) (smulRight v x) : End K W) : (a : W) → W) z : W)
this :
  ∀ (A : End K V) (x : V),
    Eq (α := W) ((T : (a : V) → W) ((A : (a : V) → V) x : V) : W)
      ((((f : (a : End K V) → End K W) A : End K W) : (a : W) → W) ((T : (a : V) → W) x : W) : W)
surj : Function.Surjective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
⊢ ∃ (T : V ≃ₗ[K] W), ∀ (a : End K V), (f : (a : End K V) → End K W) a ∘ₗ (↑T : V →ₗ[K] W) = (↑T : V →ₗ[K] W) ∘ₗ a
have inj : Function.Injective.{u_2 + 1, u_3 + 1} (α := V) (β := W) (⇑T : (a : V) → W)
Tactic: have inj : Function.Injective T := fun x y hxy ↦ by
    have h_smul : smulRightₗ v x = smulRightₗ v y := by
      apply f.injective <| LinearMap.ext fun z ↦ ?_
      obtain ⟨w, rfl⟩ := surj z
      simp_rw [← this, smulRightₗ_apply_apply, _root_.map_smul, hxy]
    simpa [huv.isUnit.smul_left_cancel] using congr((fun f ↦ f u) $h_smul)
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Semifield K
inst_1 : AddCommMonoid V
inst_2 : Module K V
inst_3 : Projective K V
f : End K V ≃ₐ[K] End K V
⊢ ∃ (a : ConjAct (GeneralLinearGroup K V)), MulSemiringAction.toAlgEquiv K (End K V) a = f
have have : ∀ (T : V ≃ₗ[K] V) (hT : f = conjAlgEquiv K T),
  ∃ (a : ConjAct (GeneralLinearGroup K V)), MulSemiringAction.toAlgEquiv K (End K V) a = f
Tactic: have ⟨T, hT⟩ := f.eq_linearEquivConjAlgEquiv
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
x y : GeneralLinearGroup R M
⊢ (x * y).toLinearEquiv = x.toLinearEquiv * y.toLinearEquiv
have h : ∀ (x_1 : M),
  Eq (α := M) (((x * y).toLinearEquiv : (a : M) → M) x_1 : M)
    ((x.toLinearEquiv * y.toLinearEquiv : (a : M) → M) x_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.GeneralLinearGroup.Basic (goal)
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
⊢ (↑((generalLinearEquiv R M : (a : GeneralLinearGroup R M) → M ≃ₗ[R] M) f) : M →ₗ[R] M) = (↑f : M →ₗ[R] M)
have h : ∀ (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: ext
-- 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)
⊢ L.goursatFst.toAddSubgroup = AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup
have h : ∀ (x : M),
  x ∈ L.goursatFst.toAddSubgroup ↔
    Membership.mem (γ := AddSubgroup M) (AddSubgroup.goursatFst.{u_2, u_3} (H := N) L.toAddSubgroup) x
Tactic: ext x
-- 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)
⊢ L.goursatSnd.toAddSubgroup = AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup
have h : ∀ (x : N),
  x ∈ L.goursatSnd.toAddSubgroup ↔
    Membership.mem (γ := AddSubgroup N) (AddSubgroup.goursatSnd.{u_2, u_3} (G := M) L.toAddSubgroup) x
Tactic: ext x
-- 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 : 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
have 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
Tactic: obtain ⟨(e : M ⧸ L.goursatFst ≃+ N ⧸ L.goursatSnd), he⟩ :=
    L.toAddSubgroup.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)
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)
have change : (r • x, HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)) ∈
  e.toAddMonoidHom.graph
Tactic: change (r • x, r • e x) ∈ e.toAddMonoidHom.graph
-- 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
r : R
x : M ⧸ L.goursatFst
⊢ (r • x,
      HSMul.hSMul (β := N ⧸ L.goursatSnd) r ((e : (a : M ⧸ L.goursatFst) → N ⧸ L.goursatSnd) x : N ⧸ L.goursatSnd)) ∈
    e.toAddMonoidHom.graph
have 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)))
Tactic: rw [← he, ← Prod.smul_mk]
-- 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)
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 (γ := 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)))
have 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))
Tactic: have : (x, e x) ∈ e.toAddMonoidHom.graph := rfl
-- 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)
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))
⊢ 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)))
have this₁ : ∃ (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
Cleared hypotheses: this
-- 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
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))
⊢ 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)))
have 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) sorry) =
  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⟩
-- 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)
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
⊢ ∃ (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
have 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)
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
-- 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 : 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
have h : (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range =
  graph
    (↑{ toFun := e.toFun, map_add' := sorry, map_smul' := this, invFun := e.invFun, left_inv := sorry, right_inv := sorry } :
      M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd)
Tactic: use { e with map_smul' := this }
-- 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)
⊢ (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)
have h : (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range.toAddSubgroup =
  toAddSubgroup (module_M := Prod.instModule)
    (graph
      (↑{ toFun := e.toFun, map_add' := sorry, map_smul' := this, invFun := e.invFun, left_inv := sorry, right_inv := sorry } :
        M ⧸ L.goursatFst →ₗ[R] N ⧸ L.goursatSnd))
Tactic: rw [← toAddSubgroup_injective.eq_iff]
-- 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)
⊢ (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))
have 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' := 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)) =
    e.toAddMonoidHom.graph
Tactic: convert! he using 1