awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
      (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M)))
    (∑ x_1 ∈ DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y),
      HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
        (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
            (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) x_1) : M) :
          ⨁ (i : ιM), ↥(𝓜 i)))
have refine : ∀ (j : ιM)
  (_hj :
    Membership.mem (γ := Finset ιM)
      (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j),
  (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
        (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) =
    HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
      (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M) :
        ⨁ (i : ιM), ↥(𝓜 i))
Tactic: refine Finset.sum_congr rfl (fun j _hj => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
j : ιM
_hj :
  Membership.mem (γ := Finset ιM)
    (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j
⊢ (decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
        (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) =
    HSMul.hSMul (β := ⨁ (i : ιM), ↥(𝓜 i))
      (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M) :
        ⨁ (i : ιM), ↥(𝓜 i))
have rw : Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
  ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
        (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
    ⨁ (i : ιM), ↥(𝓜 i))
  ((((Gmodule.smulAddMonoidHom (fun (i : ιA) ↦ ↥(𝓐 i)) fun (i : ιM) ↦ ↥(𝓜 i) :
              (a : ⨁ (i : ιA), ↥(𝓐 i)) → (⨁ (i : ιM), ↥(𝓜 i)) →+ ⨁ (i : ιM), ↥(𝓜 i))
            ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i))
              (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)) :
          (⨁ (i : ιM), ↥(𝓜 i)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
        (a : ⨁ (i : ιM), ↥(𝓜 i)) → ⨁ (i : ιM), ↥(𝓜 i))
      ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
    ⨁ (i : ιM), ↥(𝓜 i))
Tactic: rw [show (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
    DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i))
    (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j)) from DirectSum.Gmodule.smul_def _ _ _ _]
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
j : ιM
_hj :
  Membership.mem (γ := Finset ιM)
    (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))
    ((((Gmodule.smulAddMonoidHom (fun (i : ιA) ↦ ↥(𝓐 i)) fun (i : ιM) ↦ ↥(𝓜 i) :
                (a : ⨁ (i : ιA), ↥(𝓐 i)) → (⨁ (i : ιM), ↥(𝓜 i)) →+ ⨁ (i : ιM), ↥(𝓜 i))
              ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i))
                (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) :
                  A)) :
            (⨁ (i : ιM), ↥(𝓜 i)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
          (a : ⨁ (i : ιM), ↥(𝓜 i)) → ⨁ (i : ιM), ↥(𝓜 i))
        ((decomposeAddEquiv 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))
have simp : Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
  ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
      ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
        (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
    ⨁ (i : ιM), ↥(𝓜 i))
  (((of.{u_2, u_5} (fun (i : ιM) ↦ ↥(𝓜 i)) (i +ᵥ j) : ↥(𝓜 (i +ᵥ j)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
        (a : ↥(𝓜 (i +ᵥ j))) → ⨁ (i : ιM), ↥(𝓜 i))
      (@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
        (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
        ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
        ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j)) :
    ⨁ (i : ιM), ↥(𝓜 i))
Tactic: simp only [decomposeAddEquiv_apply, decompose_coe, Gmodule.smulAddMonoidHom_apply_of_of]
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
i : ιA
_hi :
  Membership.mem (γ := Finset ιA)
    (DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x)) i
j : ιM
_hj :
  Membership.mem (γ := Finset ιM)
    (DFinsupp.support (β := fun (i : ιM) ↦ ↥(𝓜 i)) ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y)) j
⊢ Eq (α := ⨁ (i : ιM), ↥(𝓜 i))
    ((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
        ((↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
          (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M)) :
      ⨁ (i : ιM), ↥(𝓜 i))
    (((of.{u_2, u_5} (fun (i : ιM) ↦ ↥(𝓜 i)) (i +ᵥ j) : ↥(𝓜 (i +ᵥ j)) →+ ⨁ (i : ιM), ↥(𝓜 i)) :
          (a : ↥(𝓜 (i +ᵥ j))) → ⨁ (i : ιM), ↥(𝓜 i))
        (@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
          (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
          ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
          ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j)) :
      ⨁ (i : ιM), ↥(𝓜 i))
have h₁ : (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A) •
    (↑((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) : M) =
  (↑(@GradedMonoid.GSMul.smul _ _ (fun (i : ιA) ↦ ↥(𝓐 i)) (fun (i : ιM) ↦ ↥(𝓜 i))
          (@AddSemigroupAction.toVAdd _ _ AddMonoid.toAddSemigroup _) _ _ _
          ((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i)
          ((((decompose 𝓜 : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i)) : (a : ιM) → ↥(𝓜 a)) j) :
        ↥(𝓜 (i +ᵥ j))) :
    M)
Tactic: convert! DirectSum.decompose_coe 𝓜 _
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
⊢ AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (x • y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) x : A)
      (AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) y)
have rw : (AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) (x • y) =
  HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) x : A)
    ((AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
Tactic: classical
  rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul,
    AddEquiv.coe_toAddHom, map_sum, Finset.sum_smul]
  refine Finset.sum_congr rfl (fun i _hi => ?_)
  rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum,
    Finset.smul_sum]
  refine Finset.sum_congr rfl (fun j _hj => ?_)
  rw [show (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
    DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i))
    (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j)) from DirectSum.Gmodule.smul_def _ _ _ _]
  simp only [decomposeAddEquiv_apply, decompose_coe, Gmodule.smulAddMonoidHom_apply_of_of]
  convert! DirectSum.decompose_coe 𝓜 _
  rfl
-- Lean 4 proof step from Mathlib.Algebra.Module.GradedModule (goal)
Goal:
ιA : Type u_1
ιM : Type u_2
R : Type u_3
A : Type u_4
M : Type u_5
σ : Type u_6
σ' : Type u_7
inst : AddMonoid ιA
inst_1 : AddAction ιA ιM
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Algebra R A
𝓐 : ιA → σ'
inst_5 : SetLike σ' A
𝓜 : ιM → σ
inst_6 : AddCommMonoid M
inst_7 : Module A M
inst_8 : SetLike σ M
inst_9 : AddSubmonoidClass σ' A
inst_10 : AddSubmonoidClass σ M
inst_11 : SetLike.GradedMonoid 𝓐
inst_12 : SetLike.GradedSMul 𝓐 𝓜
inst_13 : DecidableEq ιA
inst_14 : DecidableEq ιM
inst_15 : GradedRing 𝓐
inst_16 : Decomposition 𝓜
h : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
x : A
y : M
rw :
  (AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) (x • y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) x : A)
      ((AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
⊢ AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (x • y) =
    HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) x : A)
      (AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) y)
have rw₁ : (AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i))
    (HSMul.hSMul.{u_4, u_5, u_5} (α := A)
      (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
        (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A))
      y) =
  HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i))
    ((RingHom.id A : (a : A) → A)
        (∑ i ∈ DFinsupp.support (β := fun (i : ιA) ↦ ↥(𝓐 i)) ((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x),
          (↑((((decompose 𝓐 : (a : A) → ⨁ (i : ιA), ↥(𝓐 i)) x : ⨁ (i : ιA), ↥(𝓐 i)) : (a : ιA) → ↥(𝓐 a)) i) : A)) :
      A)
    ((AddEquiv.toAddHom (decomposeAddEquiv 𝓜) : (a : M) → ⨁ (i : ιM), ↥(𝓜 i)) y : ⨁ (i : ιM), ↥(𝓜 i))
Tactic: classical
  rw [AddHom.toFun_eq_coe, ← DirectSum.sum_support_decompose 𝓐 x, map_sum, Finset.sum_smul,
    AddEquiv.coe_toAddHom, map_sum, Finset.sum_smul]
  refine Finset.sum_congr rfl (fun i _hi => ?_)
  rw [RingHom.id_apply, ← DirectSum.sum_support_decompose 𝓜 y, map_sum, Finset.smul_sum, map_sum,
    Finset.smul_sum]
  refine Finset.sum_congr rfl (fun j _hj => ?_)
  rw [show (decompose 𝓐 x i : A) • (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j) : (⨁ i, 𝓜 i)) =
    DirectSum.Gmodule.smulAddMonoidHom _ _ (decompose 𝓐 ↑(decompose 𝓐 x i))
    (decomposeAddEquiv 𝓜 ↑(decompose 𝓜 y j)) from DirectSum.Gmodule.smul_def _ _ _ _]
  simp only [decomposeAddEquiv_apply, decompose_coe, Gmodule.smulAddMonoidHom_apply_of_of]
  convert! DirectSum.decompose_coe 𝓜 _
  rfl
-- Lean 4 proof step from Mathlib.Algebra.Module.Hom (goal)
Goal:
R : Type u_1
S_1 : Type u_2
M_1 : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ Eq.{u_8 + 1} (α := M₂) (((s + s') • f : (a : M) → M₂) m : M₂) ((s • f + s' • f : (a : M) → M₂) m : M₂)
have simp_rw : Eq.{u_8 + 1} (α := M₂)
  ((f : (a : M) → M₂) (HSMul.hSMul (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) (s + s') : S) m) : M₂)
  ((f : (a : M) → M₂)
      (HAdd.hAdd (α := S) (β := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) s : S)
          ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) s' : S) •
        m) :
    M₂)
Tactic: simp_rw [AddMonoidHom.add_apply, DomMulAct.smul_addMonoidHom_apply, ← map_add, ← add_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Hom (goal)
Goal:
R : Type u_1
S_1 : Type u_2
M_1 : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst : Semiring S
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module S M
x : M →+ M₂
x_1 : M
⊢ Eq.{u_8 + 1} (α := M₂) ((HSMul.hSMul (α := Sᵈᵐᵃ) 0 x : (a : M) → M₂) x_1 : M₂) ((0 : (a : M) → M₂) x_1 : M₂)
have rw : Eq.{u_8 + 1} (α := M₂)
  ((x : (a : M) → M₂) (HSMul.hSMul.{u_6, u_7, u_7} (α := S) ((Equiv.symm DomMulAct.mk : (a : Sᵈᵐᵃ) → S) 0 : S) x_1) :
    M₂)
  ((0 : (a : M) → M₂) x_1 : M₂)
Tactic: rw [DomMulAct.smul_addMonoidHom_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
⊢ Baer R M ↔
    ∀ (I : Ideal R),
      Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
        (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
have refine_1 : ∀ (h : Baer R M) (I : Ideal R) (g : ↥I →ₗ[R] M),
  ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g
Tactic: refine ⟨fun h I g ↦ ?_, fun h I g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
refine_1 :
  ∀ (h : Baer R M) (I : Ideal R) (g : ↥I →ₗ[R] M),
    ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g
⊢ Baer R M ↔
    ∀ (I : Ideal R),
      Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
        (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
have refine_2 : ∀
  (h :
    ∀ (I : Ideal R),
      Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
        (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M))
  (I : Ideal R) (g : ↥I →ₗ[R] M),
  ∃ (g' : R →ₗ[R] M),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
        ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
Tactic: refine ⟨fun h I g ↦ ?_, fun h I g ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
⊢ ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g
have refine_1 : ∀ (g' : R →ₗ[R] M)
  (hg' :
    ∀ (x : R) (mem : x ∈ I),
      Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
        ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)),
  ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g
Tactic: rcases h I g with ⟨g', hg'⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' :
  ∀ (x : R) (mem : x ∈ I),
    Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
      ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
⊢ ∃ (a : R →ₗ[R] M), (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) a = g
have h₁ : (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g
Tactic: use g'
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h : Baer R M
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' :
  ∀ (x : R) (mem : x ∈ I),
    Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
      ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
⊢ (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g
have h₁ : ∀ (x : ↥I),
  Eq.{u_1 + 1} (α := M)
    ((((LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' : ↥I →ₗ[R] M) : (a : ↥I) → M) x :
      M)
    ((g : (a : ↥I) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Ideal R
g : ↥I →ₗ[R] M
⊢ ∃ (g' : R →ₗ[R] M),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
        ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
have refine_2 : ∀ (g' : R →ₗ[R] M) (hg' : (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g),
  ∃ (g' : R →ₗ[R] M),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
        ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
Tactic: rcases h I g with ⟨g', hg'⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
M : Type u_1
inst : AddCommGroup M
R : Type u
inst_1 : CommRing R
inst_2 : Module R M
h :
  ∀ (I : Ideal R),
    Function.Surjective (α := R →ₗ[R] M) (β := ↥I →ₗ[R] M)
      (⇑(LinearMap.lcomp R M (Submodule.subtype I)) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M)
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : (LinearMap.lcomp R M (Submodule.subtype I) : (a : R →ₗ[R] M) → ↥I →ₗ[R] M) g' = g
⊢ ∃ (g' : R →ₗ[R] M),
    ∀ (x : R) (mem : x ∈ I),
      Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
        ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
have h₁ : ∀ (x : R) (mem : x ∈ I),
  Eq.{u_1 + 1} (α := M) ((g' : (a : R) → M) x : M)
    ((g : (a : ↥I) → M) (Subtype.mk (p := fun (x : R) ↦ x ∈ I) x mem) : M)
Tactic: use g'
-- Lean 4 proof step from Mathlib.Algebra.Module.Injective (goal)
Goal:
R : Type u
inst : Ring R
Q : Type v
inst_1 : AddCommGroup Q
inst_2 : Module R Q
M : Type u_1
N : Type u_2
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
domain_eq : a.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄,
    (↑a.toLinearPMap : ↥a.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ a.domain) x ha) =
      (↑b.toLinearPMap : ↥b.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ b.domain) x hb)
⊢ a = b
have rcases : ∀ (a : N →ₗ.[R] Q) (a_le : i.range ≤ a.domain)
  (e1 :
    ∀ (m : M),
      (f : (a : M) → Q) m = (↑a : ↥a.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ a.domain) ((i : (a : M) → N) m) sorry))
  (domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain = b.domain)
  (to_fun_eq :
    ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain⦄
      ⦃hb : x ∈ b.domain⦄,
      (↑{ toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.toLinearPMap :
            ↥{ toLinearPMap := a, le := a_le, is_extension := e1 }.domain → Q)
          (Subtype.mk (p := fun (x : N) ↦
            x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f }.domain) x ha) =
        (↑b.toLinearPMap : ↥b.domain → Q) (Subtype.mk (p := fun (x : N) ↦ x ∈ b.domain) x hb)),
  { toLinearPMap := a, le := a_le, is_extension := e1 : ExtensionOf i f } = b
Tactic: rcases a with ⟨a, a_le, e1⟩
Cleared hypotheses: a, domain_eq, to_fun_eq