awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
change :
  Eq.{u_3 + 1} (α := R)
    ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
      R)
    (1 : R)
⊢ Eq.{u_3 + 1} (α := R) ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) 1 : R) (1 : R)

Tactic:
change (toAddMonoid f) (of _ 0 _) = 1

Premises used: DirectSum.of, OfNat.ofNat, DFunLike.coe, DirectSum.toAddMonoid
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
rw : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
      R)
    (1 : R)

Tactic:
rw [toAddMonoid_of]

Premises used: DirectSum.toAddMonoid_of
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
⊢ Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)

Tactic:
hone
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
⊢ Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)

Tactic:
exact hone
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
rw :
  AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f) =
    (AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)
⊢ ∀ (x y : ⨁ (i : ι), A i),
    (toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) (x * y) =
      HMul.hMul (α := R) (β := R) ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) x : R)
        ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) y : R)

Tactic:
rw [(toAddMonoid f).map_mul_iff]

Premises used: AddMonoidHom.map_mul_iff, DirectSum.toAddMonoid
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f) =
    (AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)

Tactic:
DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))

Premises used: AddMonoidHom.ext, DirectSum.addHom_ext'
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
refine :
  ∀ (xi : ι) (xv : A xi),
    Eq (α := (⨁ (i : ι), A i) →+ R)
      ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f)) (of A xi) :
            (a : A xi) → (⨁ (i : ι), A i) →+ R)
          xv :
        (⨁ (i : ι), A i) →+ R)
      ((((AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)).comp (of A xi) :
            (a : A xi) → (⨁ (i : ι), A i) →+ R)
          xv :
        (⨁ (i : ι), A i) →+ R)
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f) =
    (AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)

Tactic:
refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))

Premises used: AddMonoidHom.ext, DirectSum.addHom_ext'
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
⊢ Eq (α := (⨁ (i : ι), A i) →+ R)
    ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f)) (of A xi) :
          (a : A xi) → (⨁ (i : ι), A i) →+ R)
        xv :
      (⨁ (i : ι), A i) →+ R)
    ((((AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)).comp (of A xi) :
          (a : A xi) → (⨁ (i : ι), A i) →+ R)
        xv :
      (⨁ (i : ι), A i) →+ R)

Tactic:
DirectSum.addHom_ext' (fun yi ↦ AddMonoidHom.ext (fun yv ↦ ?_))

Premises used: AddMonoidHom.ext, DirectSum.addHom_ext'
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
refine :
  ∀ (yi : ι) (yv : A yi),
    Eq.{u_3 + 1} (α := R)
      ((AddMonoidHom.comp
              ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f)) (of A xi) :
                  (a : A xi) → (⨁ (i : ι), A i) →+ R)
                xv)
              (of A yi) :
            (a : A yi) → R)
          yv :
        R)
      ((AddMonoidHom.comp
              ((((AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)).comp
                    (of A xi) :
                  (a : A xi) → (⨁ (i : ι), A i) →+ R)
                xv)
              (of A yi) :
            (a : A yi) → R)
          yv :
        R)
⊢ Eq (α := (⨁ (i : ι), A i) →+ R)
    ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid (β := A) f)) (of A xi) :
          (a : A xi) → (⨁ (i : ι), A i) →+ R)
        xv :
      (⨁ (i : ι), A i) →+ R)
    ((((AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid (β := A) f)).compl₂ (toAddMonoid (β := A) f)).comp (of A xi) :
          (a : A xi) → (⨁ (i : ι), A i) →+ R)
        xv :
      (⨁ (i : ι), A i) →+ R)

Tactic:
refine DirectSum.addHom_ext' (fun yi ↦ AddMonoidHom.ext (fun yv ↦ ?_))

Premises used: AddMonoidHom.ext, DirectSum.addHom_ext'
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
yi : ι
yv : A yi
toAddMonoid :
  (DirectSum.toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
      (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
        ((of A xi : (a : A xi) → ⨁ (i : ι), A i) xv : ⨁ (i : ι), A i)
        ((of A yi : (a : A yi) → ⨁ (i : ι), A i) yv : ⨁ (i : ι), A i)) =
    HMul.hMul (α := R) (β := R)
      ((DirectSum.toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
          ((of A xi : (a : A xi) → ⨁ (i : ι), A i) xv : ⨁ (i : ι), A i) :
        R)
      ((DirectSum.toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
          ((of A yi : (a : A yi) → ⨁ (i : ι), A i) yv : ⨁ (i : ι), A i) :
        R)
⊢ Eq.{u_3 + 1} (α := R)
    ((AddMonoidHom.comp
            ((AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (DirectSum.toAddMonoid (β := A) f)) (of A xi) :
                (a : A xi) → (⨁ (i : ι), A i) →+ R)
              xv)
            (of A yi) :
          (a : A yi) → R)
        yv :
      R)
    ((AddMonoidHom.comp
            ((((AddMonoidHom.comp AddMonoidHom.mul (DirectSum.toAddMonoid (β := A) f)).compl₂
                      (DirectSum.toAddMonoid (β := A) f)).comp
                  (of A xi) :
                (a : A xi) → (⨁ (i : ι), A i) →+ R)
              xv)
            (of A yi) :
          (a : A yi) → R)
        yv :
      R)

Tactic:
change
        toAddMonoid f (of A xi xv * of A yi yv) =
          toAddMonoid f (of A xi xv) * toAddMonoid f (of A yi yv)

Premises used: HMul.hMul, DirectSum.of, DFunLike.coe, DirectSum.toAddMonoid
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
yi : ι
yv : A yi
simp_rw :
  (f (xi + yi) : (a : A (xi + yi)) → R) (GradedMonoid.GMul.mul (A := A) xv yv) =
    HMul.hMul (α := R) (β := R) ((f xi : (a : A xi) → R) xv : R) ((f yi : (a : A yi) → R) yv : R)
⊢ (toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
      (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
        ((of A xi : (a : A xi) → ⨁ (i : ι), A i) xv : ⨁ (i : ι), A i)
        ((of A yi : (a : A yi) → ⨁ (i : ι), A i) yv : ⨁ (i : ι), A i)) =
    HMul.hMul (α := R) (β := R)
      ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
          ((of A xi : (a : A xi) → ⨁ (i : ι), A i) xv : ⨁ (i : ι), A i) :
        R)
      ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
          ((of A yi : (a : A yi) → ⨁ (i : ι), A i) yv : ⨁ (i : ι), A i) :
        R)

Tactic:
simp_rw [of_mul_of, toAddMonoid_of]

Premises used: DirectSum.of_mul_of, DirectSum.toAddMonoid_of
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ (f (xi + yi) : (a : A (xi + yi)) → R) (GradedMonoid.GMul.mul (A := A) xv yv) =
    HMul.hMul (α := R) (β := R) ((f xi : (a : A xi) → R) xv : R) ((f yi : (a : A yi) → R) yv : R)

Tactic:
hmul _ _
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ (f (xi + yi) : (a : A (xi + yi)) → R) (GradedMonoid.GMul.mul (A := A) xv yv) =
    HMul.hMul (α := R) (β := R) ((f xi : (a : A xi) → R) xv : R) ((f yi : (a : A yi) → R) yv : R)

Tactic:
exact hmul _ _
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
i : ι
x : A i
⊢ Eq.{u_3 + 1} (α := R)
    ((toSemiring (A := A) f hone @hmul : (a : ⨁ (i : ι), A i) → R)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) x : ⨁ (i : ι), A i) :
      R)
    ((f i : (a : A i) → R) x : R)

Tactic:
toAddMonoid_of f i x

Premises used: Multiset.sum, Multiset.foldr, List.foldr, DirectSum.toAddMonoid_of, Finset.sum, Trunc.lift
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
⊢ (↑(toSemiring (A := A) f hone @hmul) : (⨁ (i : ι), A i) →+ R) = toAddMonoid (β := A) f

Tactic:
rfl

Premises used: AddMonoidHomClass.toAddMonoidHom, DFinsupp.sumZeroHom, DFinsupp.sumAddHom, DirectSum, DirectSum.toAddMonoid, rfl, Trunc.lift
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
i : ι
⊢ AddMonoidHom.{u_2, u_3} (A i) R

Tactic:
exact (F : (⨁ i, A i) →+ R).comp (of _ i)

Premises used: AddMonoidHomClass.toAddMonoidHom, DirectSum.of, AddMonoidHom.comp
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
simp :
  Eq.{u_3 + 1} (α := R)
    (((↑F : (⨁ (i : ι), A i) →+ R) : (a : ⨁ (i : ι), A i) → R)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
      R)
    (1 : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A 0) : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R)
    (1 : R)

Tactic:
simp only [AddMonoidHom.comp_apply]

Premises used: AddMonoidHom.comp_apply
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
rw :
  Eq.{u_3 + 1} (α := R)
    (((↑F : (⨁ (i : ι), A i) →+ R) : (a : ⨁ (i : ι), A i) → R)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
      R)
    ((F : (a : ⨁ (i : ι), A i) → R) 1 : R)
⊢ Eq.{u_3 + 1} (α := R)
    (((↑F : (⨁ (i : ι), A i) →+ R) : (a : ⨁ (i : ι), A i) → R)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
      R)
    (1 : R)

Tactic:
rw [← F.map_one]

Premises used: RingHom.map_one
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ Eq.{u_3 + 1} (α := R)
    (((↑F : (⨁ (i : ι), A i) →+ R) : (a : ⨁ (i : ι), A i) → R)
        ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
      R)
    ((F : (a : ⨁ (i : ι), A i) → R) 1 : R)

Tactic:
rfl
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
simp :
  (F : (a : ⨁ (i : ι), A i) → R)
      ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) =
    HMul.hMul (α := R) (β := R)
      ((F : (a : ⨁ (i : ι), A i) → R) ((of A i : (a : A i) → ⨁ (i : ι), A i) ai : ⨁ (i : ι), A i) : R)
      ((F : (a : ⨁ (i : ι), A i) → R) ((of A j : (a : A j) → ⨁ (i : ι), A i) aj : ⨁ (i : ι), A i) : R)
⊢ (AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A (i + j)) : (a : A (i + j)) → R)
      (GradedMonoid.GMul.mul (A := A) ai aj) =
    HMul.hMul (α := R) (β := R) ((AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A i) : (a : A i) → R) ai : R)
      ((AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A j) : (a : A j) → R) aj : R)

Tactic:
simp only [AddMonoidHom.comp_apply, AddMonoidHom.coe_coe]

Premises used: AddMonoidHom.coe_coe, AddMonoidHom.comp_apply
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
rw :
  Eq.{u_3 + 1} (α := R)
    ((F : (a : ⨁ (i : ι), A i) → R)
        ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) :
      R)
    ((F : (a : ⨁ (i : ι), A i) → R)
        (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
          ((of A i : (a : A i) → ⨁ (i : ι), A i) ai : ⨁ (i : ι), A i)
          ((of A j : (a : A j) → ⨁ (i : ι), A i) aj : ⨁ (i : ι), A i)) :
      R)
rw₁ rw₂ :
  Eq.{u_3 + 1} (α := R)
    ((F : (a : ⨁ (i : ι), A i) → R)
        ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) :
      R)
    ((F : (a : ⨁ (i : ι), A i) → R)
        ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) :
      R)
⊢ (F : (a : ⨁ (i : ι), A i) → R)
      ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) : ⨁ (i : ι), A i) =
    HMul.hMul (α := R) (β := R)
      ((F : (a : ⨁ (i : ι), A i) → R) ((of A i : (a : A i) → ⨁ (i : ι), A i) ai : ⨁ (i : ι), A i) : R)
      ((F : (a : ⨁ (i : ι), A i) → R) ((of A j : (a : A j) → ⨁ (i : ι), A i) aj : ⨁ (i : ι), A i) : R)

Tactic:
rw [← F.map_mul (of A i ai), of_mul_of ai]

Premises used: DirectSum.of_mul_of, DirectSum.of, RingHom.map_mul, DFunLike.coe
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f :
  { f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R //
    Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
      ∀ {i j : ι} (ai : A i) (aj : A j),
        (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
          HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R) }
xi : ι
xv : A xi
⊢ Eq.{u_3 + 1} (α := R)
    (((↑((fun (F : (⨁ (i : ι), A i) →+* R) ↦
                  Subtype.mk (p := fun (f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R) ↦
                    Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
                      ∀ {i j : ι} (ai : A i) (aj : A j),
                        (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                          HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R) ((f : (a : A j) → R) aj : R))
                    (fun {i : ι} ↦ AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A i)) ⋯)
                ((fun
                      (f :
                        { f : {i : ι} → AddMonoidHom.{u_2, u_3} (A i) R //
                          Eq.{u_3 + 1} (α := R) ((f : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R) ∧
                            ∀ {i j : ι} (ai : A i) (aj : A j),
                              (f : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
                                HMul.hMul (α := R) (β := R) ((f : (a : A i) → R) ai : R)
                                  ((f : (a : A j) → R) aj : R) }) ↦
                    (toSemiring (A := A) (fun (x : ι) ↦ (↑f : {i : ι} → A i →+ R)) ⋯ ⋯ : (⨁ (i : ι), A i) →+* R))
                  f)) :
            {i : ι} → A i →+ R) :
          (a : A xi) → R)
        xv :
      R)
    (((↑f : {i : ι} → A i →+ R) : (a : A xi) → R) xv : R)

Tactic:
toAddMonoid_of (fun _ => f.1) xi xv

Premises used: Multiset.sum, Multiset.foldr, Function.update, List.map, Pi.single, Subtype.val, List.foldr, DirectSum.toAddMonoid_of, Finset.sum, Trunc.lift