awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (0 + i) : (a : A (0 + i)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) xi) :
      ⨁ (i : ι), A i)
    ((of A (i + 0) : (a : A (i + 0)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) xi ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
      ⨁ (i : ι), A i)

Tactic:
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.commutes r ⟨i, xi⟩)

Premises used: DFinsupp.single_eq_of_sigma_eq, DirectSum.GAlgebra.commutes, Sigma.mk
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
change :
  Eq (α := ⨁ (i : ι), A i)
    ((DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i) x : ⨁ (i : ι), A i)
    ((((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        x :
      ⨁ (i : ι), A i)
⊢ r • x =
    HMul.hMul (α := ⨁ (i : ι), A i)
      (({
              toFun :=
                (⇑(AddMonoidHom.comp (N := A 0) (of A 0) (@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _)) :
                  (a : R) → ⨁ (i : ι), A i),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } :
            (a : R) → ⨁ (i : ι), A i)
          r :
        ⨁ (i : ι), A i)
      x

Tactic:
change DistribSMul.toAddMonoidHom _ r x = AddMonoidHom.mul (DirectSum.of _ _ _) x

Premises used: AddMonoidHom.mul, DirectSum.of, DistribSMul.toAddMonoidHom, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
apply :
  Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) (DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r)
    ((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)))
⊢ Eq (α := ⨁ (i : ι), A i)
    ((DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i) x : ⨁ (i : ι), A i)
    ((((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        x :
      ⨁ (i : ι), A i)

Tactic:
apply DFunLike.congr_fun _ x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
H :
  ∀ (i : ι) (xi : A i),
    Eq (α := ⨁ (i : ι), A i)
      ((AddMonoidHom.comp (DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r) (of A i) : (a : A i) → ⨁ (i : ι), A i) xi :
        ⨁ (i : ι), A i)
      ((AddMonoidHom.comp
              ((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                ((of A 0 : (a : A 0) → ⨁ (i : ι), A i)
                  ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)))
              (of A i) :
            (a : A i) → ⨁ (i : ι), A i)
          xi :
        ⨁ (i : ι), A i)
⊢ Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) (DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r)
    ((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)))

Tactic:
ext i xi : 2
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
H :
  HSMul.hSMul (β := ⨁ (i : ι), A i) r ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (i : ι), A i) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) :
        ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((AddMonoidHom.comp (DistribSMul.toAddMonoidHom (⨁ (i : ι), A i) r) (of A i) : (a : A i) → ⨁ (i : ι), A i) xi :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.comp
            ((AddMonoidHom.mul : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r)))
            (of A i) :
          (a : A i) → ⨁ (i : ι), A i)
        xi :
      ⨁ (i : ι), A i)

Tactic:
dsimp only [AddMonoidHom.comp_apply, DistribSMul.toAddMonoidHom_apply,
      AddMonoidHom.mul_apply]

Premises used: AddMonoidHom.mul_apply, DistribSMul.toAddMonoidHom_apply, AddMonoidHom.comp_apply
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
H :
  Eq (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) (r • xi) : ⨁ (i : ι), A i)
    ((of A (0 + i) : (a : A (0 + i)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) xi) :
      ⨁ (i : ι), A i)
⊢ HSMul.hSMul (β := ⨁ (i : ι), A i) r ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (i : ι), A i) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) :
        ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (i : ι), A i)

Tactic:
rw [DirectSum.of_mul_of, ← of_smul]

Premises used: DirectSum.of_smul, DirectSum.of_mul_of
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
r : R
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ Eq (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) (r • xi) : ⨁ (i : ι), A i)
    ((of A (0 + i) : (a : A (0 + i)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) xi) :
      ⨁ (i : ι), A i)

Tactic:
apply DFinsupp.single_eq_of_sigma_eq (GAlgebra.smul_def r ⟨i, xi⟩)

Premises used: DFinsupp.single_eq_of_sigma_eq, DirectSum.GAlgebra.smul_def, Sigma.mk
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : GAlgebra R A
inst_6 : DecidableEq ι
r : R
⊢ Eq (α := ⨁ (i : ι), A i) ((algebraMap R (⨁ (i : ι), A i) : (a : R) → ⨁ (i : ι), A i) r : ⨁ (i : ι), A i)
    ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) ((@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _ : (a : R) → A 0) r) :
      ⨁ (i : ι), A i)

Tactic:
rfl

Premises used: DFinsupp.single, rfl
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : GAlgebra R A
inst_6 : DecidableEq ι
⊢ Eq (α := R →+ ⨁ (i : ι), A i) (↑(algebraMap R (⨁ (i : ι), A i)) : R →+ ⨁ (i : ι), A i)
    (AddMonoidHom.comp (N := A 0) (of A 0) (@GAlgebra.toFun _ _ A _ _ inst_2 _ inst_4 _))

Tactic:
rfl

Premises used: DFinsupp.single, rfl
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, uA, uB} (RingHom.id R) (A i) B
hone : Eq.{uB + 1} (α := B) ((f 0 : (a : A 0) → B) (GradedMonoid.GOne.one (A := A)) : B) (1 : B)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → B) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := B) (β := B) ((f i : (a : A i) → B) ai : B) ((f j : (a : A j) → B) aj : B)
r : R
change :
  Eq.{uB + 1} (α := B)
    ((toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B)
        ((algebraMap R (⨁ (i : ι), A i) : (a : R) → ⨁ (i : ι), A i) r : ⨁ (i : ι), A i) :
      B)
    ((algebraMap R B : (a : R) → B) r : B)
⊢ Eq.{uB + 1} (α := B)
    ((toSemiring (A := A) (fun (i : ι) ↦ (f i).toAddMonoidHom) hone @hmul : (a : ⨁ (i : ι), A i) → B)
        ((algebraMap R (⨁ (i : ι), A i) : (a : R) → ⨁ (i : ι), A i) r : ⨁ (i : ι), A i) :
      B)
    ((algebraMap R B : (a : R) → B) r : B)

Tactic:
change toModule R _ _ f (algebraMap R _ r) = _

Premises used: Algebra.algebraMap, DirectSum.toModule, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
f : (i : ι) → LinearMap.{uR, uR, uA, uB} (RingHom.id R) (A i) B
hone : Eq.{uB + 1} (α := B) ((f 0 : (a : A 0) → B) (GradedMonoid.GOne.one (A := A)) : B) (1 : B)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → B) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := B) (β := B) ((f i : (a : A i) → B) ai : B) ((f j : (a : A j) → B) aj : B)
r : R
rw :
  Eq.{uB + 1} (α := B)
    ((toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B) (HSMul.hSMul (β := ⨁ (i : ι), A i) r 1) : B)
    ((algebraMap R B : (a : R) → B) r : B)
rw₁ :
  (toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B) (HSMul.hSMul (β := ⨁ (i : ι), A i) r 1) =
    HSMul.hSMul (β := B) r 1
rw₂ : HSMul.hSMul (β := B) r ((toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B) 1 : B) = HSMul.hSMul (β := B) r 1
rw₃ :
  HSMul.hSMul (β := B) r
      ((toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B)
          ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
        B) =
    HSMul.hSMul (β := B) r 1
rw₄ :
  HSMul.hSMul (β := B) r
      ((toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B)
          ((lof R ι A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
        B) =
    HSMul.hSMul (β := B) r 1
rw₅ : HSMul.hSMul (β := B) r ((f 0 : (a : A 0) → B) (GradedMonoid.GOne.one (A := A)) : B) = HSMul.hSMul (β := B) r 1
rw₆ rw₇ : HSMul.hSMul (β := B) r 1 = HSMul.hSMul (β := B) r 1
⊢ Eq.{uB + 1} (α := B)
    ((toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B)
        ((algebraMap R (⨁ (i : ι), A i) : (a : R) → ⨁ (i : ι), A i) r : ⨁ (i : ι), A i) :
      B)
    ((algebraMap R B : (a : R) → B) r : B)

Tactic:
rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]

Premises used: DirectSum.one_def, DirectSum.lof_eq_of, Algebra.algebraMap_eq_smul_one, DirectSum.toModule_lof, map_smul
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
f g : (⨁ (i : ι), A i) →ₐ[R] B
h : ∀ (i : ι), f.toLinearMap ∘ₗ lof R ι A i = g.toLinearMap ∘ₗ lof R ι A i
⊢ f = g

Tactic:
AlgHom.toLinearMap_injective <| DirectSum.linearMap_ext _ h

Premises used: DirectSum.linearMap_ext, AlgHom.toLinearMap_injective
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
f g : (⨁ (i : ι), A i) →ₐ[R] B
h :
  ∀ (i : ι) (x : A i),
    Eq.{uB + 1} (α := B) ((f : (a : ⨁ (i : ι), A i) → B) ((of A i : (a : A i) → ⨁ (i : ι), A i) x : ⨁ (i : ι), A i) : B)
      ((g : (a : ⨁ (i : ι), A i) → B) ((of A i : (a : A i) → ⨁ (i : ι), A i) x : ⨁ (i : ι), A i) : B)
⊢ f = g

Tactic:
algHom_ext' R A fun i => LinearMap.ext <| h i

Premises used: LinearMap.ext, DirectSum.algHom_ext'
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
i j : ι
a : A i
r : R
x : A j
⊢ GradedMonoid.GMul.mul (A := A) a (r • x) =
    HSMul.hSMul (α := R) (β := A (i + j)) ((RingHom.id R : (a : R) → R) r : R) (GradedMonoid.GMul.mul (A := A) a x)

Tactic:
injection (smul_comm r (GradedMonoid.mk _ a) (GradedMonoid.mk _ x)).symm

Premises used: SMulCommClass.smul_comm, Eq.symm, GradedMonoid.mk
-- Module: Mathlib.Algebra.DirectSum.Algebra
Goal:
ι : Type uι
R : Type uR
A : ι → Type uA
B : Type uB
inst : CommSemiring R
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : (i : ι) → Module.{uR, uA} R (A i)
inst_3 : AddMonoid ι
inst_4 : GSemiring A
inst_5 : Semiring B
inst_6 : GAlgebra R A
inst_7 : Algebra R B
inst_8 : DecidableEq ι
i j : ι
r : R
x : A i
y : A j
⊢ Eq (α := A (i + j))
    (({ toFun := fun (b : A j) ↦ GradedMonoid.GMul.mul (A := A) (r • x) b, map_add' := ⋯, map_smul' := ⋯ } :
          (a : A j) → A (i + j))
        y :
      A (i + j))
    ((HSMul.hSMul (α := R) (β := A j →ₗ[R] A (i + j)) ((RingHom.id R : (a : R) → R) r : R)
            { toFun := fun (b : A j) ↦ GradedMonoid.GMul.mul (A := A) x b, map_add' := ⋯, map_smul' := ⋯ :
              A j →ₗ[R] A (i + j) } :
          (a : A j) → A (i + j))
        y :
      A (i + j))

Tactic:
injection smul_assoc r (GradedMonoid.mk _ x) (GradedMonoid.mk _ y)

Premises used: smul_assoc, GradedMonoid.mk
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
v : ⨁ (i : ι), β i
⊢ (coeFnAddMonoidHom β : (a : ⨁ (i : ι), β i) → (i : ι) → β i) v = (⇑v : (a : ι) → β a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommGroup (β i)
g₁ g₂ : ⨁ (i : ι), β i
i : ι
⊢ (g₁ - g₂ : (a : ι) → β a) i = (g₁ : (a : ι) → β a) i - (g₂ : (a : ι) → β a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
x y : DirectSum ι β
w : ∀ (i : ι), (x : (a : ι) → β a) i = (y : (a : ι) → β a) i
⊢ x = y

Tactic:
DFunLike.ext _ _ w

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
i : ι
⊢ (0 : (a : ι) → β a) i = 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
g₁ g₂ : ⨁ (i : ι), β i
i : ι
⊢ (g₁ + g₂ : (a : ι) → β a) i = (g₁ : (a : ι) → β a) i + (g₂ : (a : ι) → β a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
α : Type u_1
s : Finset α
g : α → ⨁ (i : ι), β i
i : ι
⊢ (∑ a ∈ s, g a : (a : ι) → β a) i = ∑ a ∈ s, (g a : (a : ι) → β a) i

Tactic:
DFinsupp.finsetSum_apply s g i

Premises used: DFinsupp.finsetSum_apply, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
i : ι
x : β i
⊢ (((of β i : (a : β i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i) : (a : ι) → β a) i = x

Tactic:
DFinsupp.single_eq_same

Premises used: DFinsupp.single_eq_same
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
i j : ι
x : β i
h : j ≠ i
⊢ (((of β i : (a : β i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i) : (a : ι) → β a) j = 0

Tactic:
DFinsupp.single_eq_of_ne h

Premises used: DFinsupp.single_eq_of_ne
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
i j : ι
x : β i
⊢ (((of β i : (a : β i) → ⨁ (i : ι), β i) x : ⨁ (i : ι), β i) : (a : ι) → β a) j =
    if h : i = j then Eq.recOn (motive := fun (x : ι) (x_1 : i = x) ↦ β x) h x else 0

Tactic:
DFinsupp.single_apply

Premises used: DFinsupp.single_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
s : Finset ι
f : (i : (↑(↑s : Set ι) : Type v)) → β (↑i : ι)
n : ι
hn : n ∈ s
⊢ (((mk β s : (a : (i : (↑(↑s : Set ι) : Type v)) → β (↑i : ι)) → ⨁ (i : ι), β i) f : ⨁ (i : ι), β i) : (a : ι) → β a)
      n =
    f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) n hn)

Tactic:
DFinsupp.mk_of_mem hn

Premises used: DFinsupp.mk_of_mem
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
s : Finset ι
f : (i : (↑(↑s : Set ι) : Type v)) → β (↑i : ι)
n : ι
hn : n ∉ s
⊢ (((mk β s : (a : (i : (↑(↑s : Set ι) : Type v)) → β (↑i : ι)) → ⨁ (i : ι), β i) f : ⨁ (i : ι), β i) : (a : ι) → β a)
      n =
    0

Tactic:
DFinsupp.mk_of_notMem hn

Premises used: DFinsupp.mk_of_notMem
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
⊢ Eq.{v + 1} (α := Finset ι) (DFinsupp.support (β := fun (i : ι) ↦ β i) 0) ∅

Tactic:
DFinsupp.support_zero

Premises used: DFinsupp.support_zero
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
x : β i
h : x ≠ 0
⊢ Eq (α := Finset ι) (DFinsupp.support (β := fun (i : ι) ↦ β i) ((of β i : (a : β i) → ⨁ (i : ι), β i) x)) {i}

Tactic:
DFinsupp.support_single h

Premises used: DFinsupp.single, DFinsupp.support_single
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
i : ι
b : β i
⊢ Subset (α := Finset ι) (DFinsupp.support (β := fun (i : ι) ↦ β i) ((of β i : (a : β i) → ⨁ (i : ι), β i) b)) {i}

Tactic:
DFinsupp.support_single_subset

Premises used: Set.Mem, DFinsupp.single, setOf, DFinsupp.support_single_subset
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)
x : ⨁ (i : ι), β i
⊢ ∑ i ∈ DFinsupp.support (β := fun (i : ι) ↦ β i) x, (of β i : (a : β i) → ⨁ (i : ι), β i) ((x : (a : ι) → β a) i) = x

Tactic:
DFinsupp.sum_single

Premises used: DFinsupp.single, DFinsupp.sum, DirectSum, DFinsupp.sum_single
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
inst_2 : Fintype ι
x : ⨁ (i : ι), β i
w :
  ∀ (i : ι),
    (∑ i : ι, (of β i : (a : β i) → ⨁ (i : ι), β i) ((x : (a : ι) → β a) i) : (a : ι) → β a) i = (x : (a : ι) → β a) i
⊢ ∑ i : ι, (of β i : (a : β i) → ⨁ (i : ι), β i) ((x : (a : ι) → β a) i) = x

Tactic:
ext i
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
inst_2 : Fintype ι
x : ⨁ (i : ι), β i
i : ι
⊢ (∑ i : ι, (of β i : (a : β i) → ⨁ (i : ι), β i) ((x : (a : ι) → β a) i) : (a : ι) → β a) i = (x : (a : ι) → β a) i

Tactic:
simp [of_apply]

Premises used: DirectSum.of_apply
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
s : Finset ι
⊢ Injective (α := (i : (↑(↑s : Set ι) : Type v)) → β (↑i : ι)) (β := ⨁ (i : ι), β i)
    (⇑(mk β s) : (a : (i : (↑(↑s : Set ι) : Type v)) → β (↑i : ι)) → ⨁ (i : ι), β i)

Tactic:
DFinsupp.mk_injective s

Premises used: DFinsupp.mk, DFinsupp.mk_injective, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
i : ι
⊢ Injective (α := β i) (β := ⨁ (i : ι), β i) (⇑(of β i) : (a : β i) → ⨁ (i : ι), β i)

Tactic:
DFinsupp.single_injective

Premises used: DFinsupp.single, DFinsupp.single_injective, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i : (a : β i) → ⨁ (i : ι), β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
apply :
  ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    (f : (a : ι) → β a) i = 0 → b ≠ 0 → motive f → motive (DFinsupp.single (β := fun (i : ι) ↦ β i) i b + f)
⊢ motive x

Tactic:
apply DFinsupp.induction x zero

Premises used: DFinsupp.induction
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
x : ⨁ (i : ι), β i
zero : motive 0
of : ∀ (i : ι) (x : β i), motive ((DirectSum.of β i : (a : β i) → ⨁ (i : ι), β i) x)
add : ∀ (x y : ⨁ (i : ι), β i), motive x → motive y → motive (x + y)
i : ι
b : β i
f : Π₀ (i : ι), β i
h1 : (f : (a : ι) → β a) i = 0
h2 : b ≠ 0
ih : motive f
⊢ motive (DFinsupp.single (β := fun (i : ι) ↦ β i) i b + f)

Tactic:
solve_by_elim
-- Module: Mathlib.Algebra.DirectSum.Basic
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
motive : (⨁ (i : ι), β i) → Prop
f : ⨁ (i : ι), β i
h0 : motive 0
hadd :
  ∀ (i : ι) (b : β i) (f : ⨁ (i : ι), β i),
    (f : (a : ι) → β a) i = 0 →
      b ≠ 0 →
        motive f → motive (HAdd.hAdd (α := ⨁ (i : ι), β i) ((of β i : (a : β i) → ⨁ (i : ι), β i) b : ⨁ (i : ι), β i) f)
⊢ motive f

Tactic:
DFinsupp.induction f h0 hadd

Premises used: DFinsupp.induction