awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
inst_5 : FinitePresentation R M
f : M →ₗ[R] N
⊢ Eq (α := LocalizedModule S (M →ₗ[R] N))
    ((LinearEquiv.symm (linearEquivMap S) :
          (a : LocalizedModule S M →ₗ[R] LocalizedModule S N) → LocalizedModule S (M →ₗ[R] N))
        ((IsLocalizedModule.map S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N) :
            (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[R] LocalizedModule S N)
          f) :
      LocalizedModule S (M →ₗ[R] N))
    ((LocalizedModule.mkLinearMap S (M →ₗ[R] N) : (a : M →ₗ[R] N) → LocalizedModule S (M →ₗ[R] N)) f :
      LocalizedModule S (M →ₗ[R] N))

Tactic:
IsLocalizedModule.linearEquiv_symm_apply S _ _ f

Premises used: IsLocalizedModule.linearEquiv_symm_apply
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
inst_5 : FinitePresentation R M
f : M →ₗ[R] N
⊢ Eq (α :=
    LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
      (LocalizedModule S N))
    ((linearEquivMapExtendScalars S :
          (a : LocalizedModule S (M →ₗ[R] N)) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N)
        ((LocalizedModule.mkLinearMap S (M →ₗ[R] N) : (a : M →ₗ[R] N) → LocalizedModule S (M →ₗ[R] N)) f) :
      LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
        (LocalizedModule S N))
    (((IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
              (Localization (M := R) S) :
            (M →ₗ[R] N) →ₗ[R]
              LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
                (LocalizedModule S N)) :
          (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N)
        f :
      LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
        (LocalizedModule S N))

Tactic:
IsLocalizedModule.linearEquiv_apply S _ _ f

Premises used: IsLocalizedModule.linearEquiv_apply
-- Module: Mathlib.Algebra.Module.FinitePresentation
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
S : Submonoid R
inst_5 : FinitePresentation R M
f : M →ₗ[R] N
⊢ Eq (α := LocalizedModule S (M →ₗ[R] N))
    ((LinearEquiv.symm (linearEquivMapExtendScalars S) :
          (a : LocalizedModule S M →ₗ[Localization S] LocalizedModule S N) → LocalizedModule S (M →ₗ[R] N))
        (((IsLocalizedModule.mapExtendScalars S (LocalizedModule.mkLinearMap S M) (LocalizedModule.mkLinearMap S N)
                (Localization (M := R) S) :
              (M →ₗ[R] N) →ₗ[R]
                LinearMap (R := Localization (M := R) S) (RingHom.id (Localization (M := R) S)) (LocalizedModule S M)
                  (LocalizedModule S N)) :
            (a : M →ₗ[R] N) → LocalizedModule S M →ₗ[Localization S] LocalizedModule S N)
          f) :
      LocalizedModule S (M →ₗ[R] N))
    ((LocalizedModule.mkLinearMap S (M →ₗ[R] N) : (a : M →ₗ[R] N) → LocalizedModule S (M →ₗ[R] N)) f :
      LocalizedModule S (M →ₗ[R] N))

Tactic:
IsLocalizedModule.linearEquiv_symm_apply S _ _ f

Premises used: IsLocalizedModule.linearEquiv_symm_apply
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιA), A i
y : ⨁ (i : ιB), M i
⊢ x • y =
    (((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) x :
          (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
        (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
      y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
i : ιA
j : ιB
x : A i
y : M j
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              ((of A i : (a : A i) → ⨁ (i : ιA), A i) x) :
            (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M j : (a : M j) → ⨁ (i : ιB), M i) y) :
      ⨁ (i : ιB), M i)
    ((of M (i +ᵥ j) : (a : M (i +ᵥ j)) → ⨁ (i : ιB), M i) (GSMul.smul (A := A) (M := M) x y) : ⨁ (i : ιB), M i)

Tactic:
simp [smulAddMonoidHom]

Premises used: DirectSum.Gmodule.smulAddMonoidHom
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
i : ιA
j : ιB
x : A i
y : M j
⊢ HSMul.hSMul (α := ⨁ (i : ιA), A i) (β := ⨁ (i : ιB), M i) ((of A i : (a : A i) → ⨁ (i : ιA), A i) x : ⨁ (i : ιA), A i)
      ((of M j : (a : M j) → ⨁ (i : ιB), M i) y : ⨁ (i : ιB), M i) =
    (of M (i +ᵥ j) : (a : M (i +ᵥ j)) → ⨁ (i : ιB), M i) (GSMul.smul (A := A) (M := M) x y)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
suffices :
  Eq (α := (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
    ((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) 1)
    (AddMonoidHom.id (⨁ (i : ιB), M i))
⊢ HSMul.hSMul (α := ⨁ (i : ιA), A i) 1 x = x

Tactic:
suffices smulAddMonoidHom A M 1 = AddMonoidHom.id (⨁ i, M i) from DFunLike.congr_fun this x
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
H :
  ∀ (i : ιB) (y : M i),
    Eq (α := ⨁ (i : ιB), M i)
      (((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) 1 :
            (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
          ((of M i : (a : M i) → ⨁ (i : ιB), M i) y) :
        ⨁ (i : ιB), M i)
      ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
          ((of M i : (a : M i) → ⨁ (i : ιB), M i) y) :
        ⨁ (i : ιB), M i)
⊢ Eq (α := (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
    ((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) 1)
    (AddMonoidHom.id (⨁ (i : ιB), M i))

Tactic:
apply DirectSum.addHom_ext

Premises used: DirectSum.addHom_ext
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ Eq (α := ⨁ (i : ιA), A i) (1 : ⨁ (i : ιA), A i)
    ((of A 0 : (a : A 0) → ⨁ (i : ιA), A i) (GOne.one (A := A)) : ⨁ (i : ιA), A i)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
H :
  Eq (α := ⨁ (i : ιB), M i)
    ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              ((of A 0 : (a : A 0) → ⨁ (i : ιA), A i) (GOne.one (A := A))) :
            (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
⊢ Eq (α := ⨁ (i : ιB), M i)
    (((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) 1 :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)

Tactic:
rw [show (1 : DirectSum ιA fun i => A i) = (of A 0) GOne.one by rfl]
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
H :
  Eq (α := ⨁ (i : ιB), M i)
    ((of M (HVAdd.hVAdd.{u_1, u_2, u_2} (α := ιA) 0 i) : (a : M (0 +ᵥ i)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) (GOne.one (A := A)) xi) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              ((of A 0 : (a : A 0) → ⨁ (i : ιA), A i) (GOne.one (A := A))) :
            (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)

Tactic:
rw [smulAddMonoidHom_apply_of_of]

Premises used: DirectSum.Gmodule.smulAddMonoidHom_apply_of_of
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((of M (HVAdd.hVAdd.{u_1, u_2, u_2} (α := ιA) 0 i) : (a : M (0 +ᵥ i)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) (GOne.one (A := A)) xi) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)

Tactic:
DirectSum.of_eq_of_gradedMonoid_eq (one_smul (GradedMonoid A) <| GradedMonoid.mk i xi)

Premises used: DFinsupp.single, one_smul, GradedMonoid, DirectSum.of_eq_of_gradedMonoid_eq, GradedMonoid.mk
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GMonoid A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
i : ιB
xi : M i
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((of M (HVAdd.hVAdd.{u_1, u_2, u_2} (α := ιA) 0 i) : (a : M (0 +ᵥ i)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) (GOne.one (A := A)) xi) :
      ⨁ (i : ιB), M i)
    ((AddMonoidHom.id (⨁ (i : ιB), M i) : (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M i : (a : M i) → ⨁ (i : ιB), M i) xi) :
      ⨁ (i : ιB), M i)

Tactic:
exact DirectSum.of_eq_of_gradedMonoid_eq (one_smul (GradedMonoid A) <| GradedMonoid.mk i xi)

Premises used: one_smul, GradedMonoid, DirectSum.of_eq_of_gradedMonoid_eq, GradedMonoid.mk
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
a₁ :
  Eq (α := (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
    (comp
      ((compHom :
          (a : (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →
            ((⨁ (i : ιA), A i) →+ ⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
        (smulAddMonoidHom A M))
      (mulHom A))
    (AddMonoidHom.flip
      ((((compHom :
                (a :
                    ((⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                      (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →
                  ((⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
                    (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              flipHom :
            ((⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →+
              (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →
            (⨁ (i : ιA), A i) →+ (⨁ (i : ιA), A i) →+ (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
        (comp (N := (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
          ((compHom :
              (a : (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i) →
                ((⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) →+ (⨁ (i : ιB), M i) →+ (⨁ (i : ιA), A i) →+ ⨁ (i : ιB), M i)
            (AddMonoidHom.flip (smulAddMonoidHom A M)))
          (smulAddMonoidHom A M))))
⊢ (a * b) • c = a • b • c

Tactic:
suffices
    (-- `fun a b c ↦ (a * b) • c` as a bundled hom
              smulAddMonoidHom
              A M).compHom.comp
        (DirectSum.mulHom A) =
      (AddMonoidHom.compHom AddMonoidHom.flipHom <|
          (smulAddMonoidHom A M).flip.compHom.comp <| smulAddMonoidHom A M).flip
    from -- `fun a b c ↦ a • (b • c)` as a bundled hom
      DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
ai : ιA
ax : A ai
bi : ιA
bx : A bi
ci : ιB
cx : M ci
H :
  Eq (α := ⨁ (i : ιB), M i)
    ((of M ((ai + bi) +ᵥ ci) : (a : M ((ai + bi) +ᵥ ci)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) (GMul.mul (A := A) ax bx) cx) :
      ⨁ (i : ιB), M i)
    ((of M (ai +ᵥ bi +ᵥ ci) : (a : M (ai +ᵥ bi +ᵥ ci)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) ax (GSMul.smul (A := A) (M := M) bx cx)) :
      ⨁ (i : ιB), M i)
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              ((((mulHom A : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιA), A i) →+ ⨁ (i : ιA), A i)
                      ((of A ai : (a : A ai) → ⨁ (i : ιA), A i) ax) :
                    (⨁ (i : ιA), A i) →+ ⨁ (i : ιA), A i) :
                  (a : ⨁ (i : ιA), A i) → ⨁ (i : ιA), A i)
                ((of A bi : (a : A bi) → ⨁ (i : ιA), A i) bx)) :
            (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((of M ci : (a : M ci) → ⨁ (i : ιB), M i) cx) :
      ⨁ (i : ιB), M i)
    ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
              ((of A ai : (a : A ai) → ⨁ (i : ιA), A i) ax) :
            (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
          (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
        ((((smulAddMonoidHom A M : (a : ⨁ (i : ιA), A i) → (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i)
                ((of A bi : (a : A bi) → ⨁ (i : ιA), A i) bx) :
              (⨁ (i : ιB), M i) →+ ⨁ (i : ιB), M i) :
            (a : ⨁ (i : ιB), M i) → ⨁ (i : ιB), M i)
          ((of M ci : (a : M ci) → ⨁ (i : ιB), M i) cx)) :
      ⨁ (i : ιB), M i)

Tactic:
rw [smulAddMonoidHom_apply_of_of, smulAddMonoidHom_apply_of_of, DirectSum.mulHom_of_of,
    smulAddMonoidHom_apply_of_of]

Premises used: DirectSum.mulHom_of_of, DirectSum.Gmodule.smulAddMonoidHom_apply_of_of
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
ai : ιA
ax : A ai
bi : ιA
bx : A bi
ci : ιB
cx : M ci
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((of M ((ai + bi) +ᵥ ci) : (a : M ((ai + bi) +ᵥ ci)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) (GMul.mul (A := A) ax bx) cx) :
      ⨁ (i : ιB), M i)
    ((of M (ai +ᵥ bi +ᵥ ci) : (a : M (ai +ᵥ bi +ᵥ ci)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) ax (GSMul.smul (A := A) (M := M) bx cx)) :
      ⨁ (i : ιB), M i)

Tactic:
DirectSum.of_eq_of_gradedMonoid_eq
      (mul_smul (GradedMonoid.mk ai ax) (GradedMonoid.mk bi bx) (GradedMonoid.mk ci cx))

Premises used: DirectSum.of_eq_of_gradedMonoid_eq, SemigroupAction.mul_smul, GradedMonoid.mk
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
a b : ⨁ (i : ιA), A i
c : ⨁ (i : ιB), M i
ai : ιA
ax : A ai
bi : ιA
bx : A bi
ci : ιB
cx : M ci
⊢ Eq (α := ⨁ (i : ιB), M i)
    ((of M ((ai + bi) +ᵥ ci) : (a : M ((ai + bi) +ᵥ ci)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) (GMul.mul (A := A) ax bx) cx) :
      ⨁ (i : ιB), M i)
    ((of M (ai +ᵥ bi +ᵥ ci) : (a : M (ai +ᵥ bi +ᵥ ci)) → ⨁ (i : ιB), M i)
        (GSMul.smul (A := A) (M := M) ax (GSMul.smul (A := A) (M := M) bx cx)) :
      ⨁ (i : ιB), M i)

Tactic:
exact
    DirectSum.of_eq_of_gradedMonoid_eq
      (mul_smul (GradedMonoid.mk ai ax) (GradedMonoid.mk bi bx) (GradedMonoid.mk ci cx))

Premises used: DirectSum.of_eq_of_gradedMonoid_eq, SemigroupAction.mul_smul, GradedMonoid.mk
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
⊢ ∀ (x y : ⨁ (i : ιA), A i) (b : ⨁ (i : ιB), M i), (x * y) • b = x • y • b

Tactic:
mul_smul' _ _

Premises used: _private.0.DirectSum.Gmodule.mul_smul'
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
⊢ ∀ (x y : ⨁ (i : ιA), A i) (b : ⨁ (i : ιB), M i), (x * y) • b = x • y • b

Tactic:
exact mul_smul' _ _

Premises used: _private.0.DirectSum.Gmodule.mul_smul'
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
⊢ ∀ (b : ⨁ (i : ιB), M i), HSMul.hSMul (α := ⨁ (i : ιA), A i) 1 b = b

Tactic:
one_smul' _ _

Premises used: _private.0.DirectSum.Gmodule.one_smul'
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
⊢ ∀ (b : ⨁ (i : ιB), M i), HSMul.hSMul (α := ⨁ (i : ιA), A i) 1 b = b

Tactic:
exact one_smul' _ _

Premises used: _private.0.DirectSum.Gmodule.one_smul'
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
r s : ⨁ (i : ιA), A i
x : ⨁ (i : ιB), M i
⊢ (r + s) • x = r • x + s • x

Tactic:
simp only [smul_def, map_add, AddMonoidHom.add_apply]

Premises used: map_add, AddMonoidHom.add_apply, DirectSum.Gmodule.smul_def
-- Module: Mathlib.Algebra.Module.GradedModule
Goal:
ιA : Type u_1
ιB : Type u_2
A : ιA → Type u_3
M : ιB → Type u_4
inst : AddMonoid ιA
inst_1 : VAdd ιA ιB
inst_2 : (i : ιA) → AddCommMonoid (A i)
inst_3 : (i : ιB) → AddCommMonoid (M i)
inst_4 : DecidableEq ιA
inst_5 : DecidableEq ιB
inst_6 : GSemiring A
inst_7 : Gmodule A M
x : ⨁ (i : ιB), M i
⊢ HSMul.hSMul (α := ⨁ (i : ιA), A i) 0 x = 0

Tactic:
simp only [smul_def, map_zero, AddMonoidHom.zero_apply]

Premises used: AddMonoidHom.zero_apply, map_zero, DirectSum.Gmodule.smul_def
-- Module: Mathlib.Algebra.Module.GradedModule
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 𝓜
this : Module A (⨁ (i : ιM), ↥(𝓜 i)) := isModule 𝓐 𝓜
⊢ Module A (⨁ (i : ιM), ↥(𝓜 i))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Module.GradedModule
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 𝓐 𝓜
refine :
  ∀ (m : A) (x : M),
    AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) (m • x) =
      HSMul.hSMul (α := A) (β := ⨁ (i : ιM), ↥(𝓜 i)) ((RingHom.id A : (a : A) → A) m : A)
        (AddHom.toFun (AddEquiv.toAddHom (decomposeAddEquiv 𝓜)) x)
⊢ M ≃ₗ[A] ⨁ (i : ιM), ↥(𝓜 i)

Tactic:
refine ⟨⟨(DirectSum.decomposeAddEquiv 𝓜).toAddHom, ?_⟩,
    (DirectSum.decomposeAddEquiv 𝓜).symm.toFun, (DirectSum.decomposeAddEquiv 𝓜).left_inv,
    (DirectSum.decomposeAddEquiv 𝓜).right_inv⟩