awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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)
    ((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)
    ((AddMonoidHom.comp
            ((AddMonoidHom.flip 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)
have H : 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) =
  HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (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: dsimp only [AddMonoidHom.comp_apply, AddMonoidHom.mul_apply, AddMonoidHom.flip_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) xi : ⨁ (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)
have H : 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: rw [of_mul_of, of_mul_of]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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
have 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)
Tactic: change DistribSMul.toAddMonoidHom _ r x = AddMonoidHom.mul (DirectSum.of _ _ _) x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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)))
Tactic: apply DFunLike.congr_fun _ x
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)))
have 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)
Tactic: ext i xi : 2
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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)
    ((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)
have 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)
Tactic: dsimp only [AddMonoidHom.comp_apply, DistribSMul.toAddMonoidHom_apply,
      AddMonoidHom.mul_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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)
Tactic: rw [DirectSum.of_mul_of, ← of_smul]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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)
Tactic: change toModule R _ _ f (algebraMap R _ r) = _
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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)
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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)
⊢ 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)
have rw₁ : (toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B) (HSMul.hSMul (β := ⨁ (i : ι), A i) r 1) =
  HSMul.hSMul (β := B) r 1
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have rw₂ : HSMul.hSMul (β := B) r ((toModule R ι (M := A) B f : (a : ⨁ (i : ι), A i) → B) 1 : B) = HSMul.hSMul (β := B) r 1
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have 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
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have rw₅ : HSMul.hSMul (β := B) r ((f 0 : (a : A 0) → B) (GradedMonoid.GOne.one (A := A)) : B) = HSMul.hSMul (β := B) r 1
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Algebra (goal)
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
⊢ 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)
have rw₆ : HSMul.hSMul (β := B) r 1 = HSMul.hSMul (β := B) r 1
Tactic: rw [Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one, map_smul, one_def,
        ← lof_eq_of R, toModule_lof, hone]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
inst_2 : Fintype ι
x : ⨁ (i : ι), β i
⊢ ∑ i : ι, (of β i : (a : β i) → ⨁ (i : ι), β i) ((x : (a : ι) → β a) i) = x
have w : ∀ (i : ι),
  (∑ i : ι, (of β i : (a : β i) → ⨁ (i : ι), β i) ((x : (a : ι) → β a) i) : (a : ι) → β a) i = (x : (a : ι) → β a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
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)
⊢ motive x
have 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)
Tactic: apply DFinsupp.induction x zero
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Basic (goal)
Goal:
ι : Type v
β : ι → Type w
inst : (i : ι) → AddCommMonoid (β i)
inst_1 : DecidableEq ι
γ : Type u₁
inst_2 : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ Eq.{u₁ + 1} (α := γ) ((ψ : (a : ⨁ (i : ι), β i) → γ) f : γ)
    ((toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i) : (a : ⨁ (i : ι), β i) → γ) f : γ)
have e_a : ψ = toAddMonoid (β := β) fun (i : ι) ↦ ψ.comp (of β i)
Tactic: congr