awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
dsimp :
  Eq (α := Π₀ (i : ι), A i)
    ((((DFinsupp.sumAddHom (β := A) fun (x : ι) ↦
                  AddMonoidHom.flip
                    (toAddMonoid (β := A) fun (x_1 : ι) ↦
                      AddMonoidHom.flip
                        (AddMonoidHom.comp (N := A x_1 →+ A (x + x_1))
                          ((compHom :
                              (a : A (x + x_1) →+ Π₀ (i : ι), A i) → (A x_1 →+ A (x + x_1)) →+ A x_1 →+ Π₀ (i : ι), A i)
                            (of A (x + x_1)))
                          (gMulHom A))) :
                (a : Π₀ (i : ι), A i) → (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i)
              a :
            (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i) :
          (a : Π₀ (i : ι), A i) → Π₀ (i : ι), A i)
        a' :
      Π₀ (i : ι), A i)
    (DFinsupp.sum (β := fun (i : ι) ↦ A i) a fun (x : ι) (ai : A x) ↦
        DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
          (of A (x + x_1) : (a : A (x + x_1)) → Π₀ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) :
      Π₀ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((((DFinsupp.sumAddHom (β := A) fun (x : ι) ↦
                  AddMonoidHom.flip
                    (toAddMonoid (β := A) fun (x_1 : ι) ↦
                      AddMonoidHom.flip
                        (AddMonoidHom.comp (N := A x_1 →+ A (x + x_1))
                          ((compHom :
                              (a : A (x + x_1) →+ ⨁ (i : ι), A i) → (A x_1 →+ A (x + x_1)) →+ A x_1 →+ ⨁ (i : ι), A i)
                            (of A (x + x_1)))
                          (gMulHom A))) :
                (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              a :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        a' :
      ⨁ (i : ι), A i)
    (DFinsupp.sum (β := fun (i : ι) ↦ A i) a fun (x : ι) (ai : A x) ↦
        DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
          (of A (x + x_1) : (a : A (x + x_1)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) :
      ⨁ (i : ι), A i)

Tactic:
dsimp only [DirectSum]

Premises used: DirectSum
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
rw :
  Eq (α := Π₀ (i : ι), A i)
    (DFinsupp.sum (β := A) a fun (a : ι) (b : A a) ↦
      (((AddMonoidHom.flip
                  (toAddMonoid (β := A) fun (x : ι) ↦
                    AddMonoidHom.flip
                      (AddMonoidHom.comp (N := A x →+ A (a + x))
                        ((compHom : (a_1 : A (a + x) →+ Π₀ (i : ι), A i) → (A x →+ A (a + x)) →+ A x →+ Π₀ (i : ι), A i)
                          (of A (a + x)))
                        (gMulHom A))) :
                (a : A a) → (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i)
              b :
            (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i) :
          (a : Π₀ (i : ι), A i) → Π₀ (i : ι), A i)
        a')
    (DFinsupp.sum (β := fun (i : ι) ↦ A i) a fun (x : ι) (ai : A x) ↦
      DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
        (of A (x + x_1) : (a : A (x + x_1)) → Π₀ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj))
⊢ Eq (α := Π₀ (i : ι), A i)
    ((((DFinsupp.sumAddHom (β := A) fun (x : ι) ↦
                  AddMonoidHom.flip
                    (toAddMonoid (β := A) fun (x_1 : ι) ↦
                      AddMonoidHom.flip
                        (AddMonoidHom.comp (N := A x_1 →+ A (x + x_1))
                          ((compHom :
                              (a : A (x + x_1) →+ Π₀ (i : ι), A i) → (A x_1 →+ A (x + x_1)) →+ A x_1 →+ Π₀ (i : ι), A i)
                            (of A (x + x_1)))
                          (gMulHom A))) :
                (a : Π₀ (i : ι), A i) → (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i)
              a :
            (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i) :
          (a : Π₀ (i : ι), A i) → Π₀ (i : ι), A i)
        a' :
      Π₀ (i : ι), A i)
    (DFinsupp.sum (β := fun (i : ι) ↦ A i) a fun (x : ι) (ai : A x) ↦
        DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
          (of A (x + x_1) : (a : A (x + x_1)) → Π₀ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj) :
      Π₀ (i : ι), A i)

Tactic:
rw [DFinsupp.sumAddHom_apply, AddMonoidHom.dfinsuppSum_apply]

Premises used: AddMonoidHom.dfinsuppSum_apply, DFinsupp.sumAddHom_apply
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
apply :
  Eq (α := (a : ι) → (b : A a) → Π₀ (i : ι), A i)
    (fun (a : ι) (b : A a) ↦
      (((AddMonoidHom.flip
                  (toAddMonoid (β := A) fun (x : ι) ↦
                    AddMonoidHom.flip
                      (AddMonoidHom.comp (N := A x →+ A (a + x))
                        ((compHom : (a_1 : A (a + x) →+ Π₀ (i : ι), A i) → (A x →+ A (a + x)) →+ A x →+ Π₀ (i : ι), A i)
                          (of A (a + x)))
                        (gMulHom A))) :
                (a : A a) → (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i)
              b :
            (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i) :
          (a : Π₀ (i : ι), A i) → Π₀ (i : ι), A i)
        a')
    fun (x : ι) (ai : A x) ↦
    DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
      (of A (x + x_1) : (a : A (x + x_1)) → Π₀ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj)
⊢ Eq (α := Π₀ (i : ι), A i)
    (DFinsupp.sum (β := A) a fun (a : ι) (b : A a) ↦
      (((AddMonoidHom.flip
                  (toAddMonoid (β := A) fun (x : ι) ↦
                    AddMonoidHom.flip
                      (AddMonoidHom.comp (N := A x →+ A (a + x))
                        ((compHom : (a_1 : A (a + x) →+ Π₀ (i : ι), A i) → (A x →+ A (a + x)) →+ A x →+ Π₀ (i : ι), A i)
                          (of A (a + x)))
                        (gMulHom A))) :
                (a : A a) → (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i)
              b :
            (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i) :
          (a : Π₀ (i : ι), A i) → Π₀ (i : ι), A i)
        a')
    (DFinsupp.sum (β := fun (i : ι) ↦ A i) a fun (x : ι) (ai : A x) ↦
      DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
        (of A (x + x_1) : (a : A (x + x_1)) → Π₀ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj))

Tactic:
apply congrArg _

Premises used: congrArg
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
h :
  ∀ (x : ι),
    Eq (α := (b : A x) → Π₀ (i : ι), A i)
      (fun (b : A x) ↦
        (((AddMonoidHom.flip
                    (toAddMonoid (β := A) fun (x_1 : ι) ↦
                      AddMonoidHom.flip
                        (AddMonoidHom.comp (N := A x_1 →+ A (x + x_1))
                          ((compHom :
                              (a : A (x + x_1) →+ Π₀ (i : ι), A i) → (A x_1 →+ A (x + x_1)) →+ A x_1 →+ Π₀ (i : ι), A i)
                            (of A (x + x_1)))
                          (gMulHom A))) :
                  (a : A x) → (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i)
                b :
              (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i) :
            (a : Π₀ (i : ι), A i) → Π₀ (i : ι), A i)
          a')
      fun (ai : A x) ↦
      DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
        (of A (x + x_1) : (a : A (x + x_1)) → Π₀ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj)
⊢ Eq (α := (a : ι) → (b : A a) → Π₀ (i : ι), A i)
    (fun (a : ι) (b : A a) ↦
      (((AddMonoidHom.flip
                  (toAddMonoid (β := A) fun (x : ι) ↦
                    AddMonoidHom.flip
                      (AddMonoidHom.comp (N := A x →+ A (a + x))
                        ((compHom : (a_1 : A (a + x) →+ Π₀ (i : ι), A i) → (A x →+ A (a + x)) →+ A x →+ Π₀ (i : ι), A i)
                          (of A (a + x)))
                        (gMulHom A))) :
                (a : A a) → (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i)
              b :
            (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i) :
          (a : Π₀ (i : ι), A i) → Π₀ (i : ι), A i)
        a')
    fun (x : ι) (ai : A x) ↦
    DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
      (of A (x + x_1) : (a : A (x + x_1)) → Π₀ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj)

Tactic:
funext x
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ Eq (α := (b : A x) → Π₀ (i : ι), A i)
    (fun (b : A x) ↦
      (((AddMonoidHom.flip
                  (toAddMonoid (β := A) fun (x_1 : ι) ↦
                    AddMonoidHom.flip
                      (AddMonoidHom.comp (N := A x_1 →+ A (x + x_1))
                        ((compHom :
                            (a : A (x + x_1) →+ Π₀ (i : ι), A i) → (A x_1 →+ A (x + x_1)) →+ A x_1 →+ Π₀ (i : ι), A i)
                          (of A (x + x_1)))
                        (gMulHom A))) :
                (a : A x) → (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i)
              b :
            (Π₀ (i : ι), A i) →+ Π₀ (i : ι), A i) :
          (a : Π₀ (i : ι), A i) → Π₀ (i : ι), A i)
        a')
    fun (ai : A x) ↦
    DFinsupp.sum (β := fun (i : ι) ↦ A i) a' fun (x_1 : ι) (aj : A x_1) ↦
      (of A (x + x_1) : (a : A (x + x_1)) → Π₀ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ai aj)

Tactic:
simp [AddMonoidHom.dfinsuppSum_apply, DFinsupp.sumAddHom_apply, DirectSum.toAddMonoid]

Premises used: AddMonoidHom.dfinsuppSum_apply, DFinsupp.sumAddHom_apply, DirectSum.toAddMonoid
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' =
    ∑ ij ∈ DFinsupp.support (β := fun (i : ι) ↦ A i) a ×ˢ DFinsupp.support (β := fun (i : ι) ↦ A i) a',
      (of A (ij.1 + ij.2) : (a : A (ij.1 + ij.2)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ((a : (a : ι) → A a) ij.1) ((a' : (a : ι) → A a) ij.2))

Tactic:
simp only [mul_eq_dfinsuppSum, DFinsupp.sum, Finset.sum_product]

Premises used: DFinsupp.sum, DirectSum.mul_eq_dfinsuppSum, Finset.sum_product
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
this : Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) (mulHom A) (AddMonoidHom.flip (mulHom A))
rw :
  (((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) a : (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
        (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
      b =
    b * a
rw₁ :
  (((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) a :
          (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
        (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
      b =
    b * a
rw₂ :
  (((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) b : (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
        (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
      a =
    b * a
rw₃ rw₄ : b * a = b * a
⊢ a * b = b * a

Tactic:
rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_apply]

Premises used: AddMonoidHom.flip_apply, DirectSum.mulHom_apply
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
suffices : Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) (mulHom A) (AddMonoidHom.flip (mulHom A))
⊢ a * b = b * a

Tactic:
suffices mulHom A = (mulHom A).flip by
    rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_apply]
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
H :
  ∀ (i : ι) (y : A i),
    Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
      ((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
          ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
        (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
      ((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
          ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
        (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
⊢ Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) (mulHom A) (AddMonoidHom.flip (mulHom A))

Tactic:
apply addHom_ext

Premises used: DirectSum.addHom_ext
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
H :
  ∀ (i : ι) (y : A i),
    Eq (α := ⨁ (i : ι), A i)
      ((((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                ((of A ai : (a : A ai) → ⨁ (i : ι), A i) ax) :
              (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
            (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
          ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
        ⨁ (i : ι), A i)
      ((((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                ((of A ai : (a : A ai) → ⨁ (i : ι), A i) ax) :
              (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
            (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
          ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
        ⨁ (i : ι), A i)
⊢ Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
        ((of A ai : (a : A ai) → ⨁ (i : ι), A i) ax) :
      (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
        ((of A ai : (a : A ai) → ⨁ (i : ι), A i) ax) :
      (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)

Tactic:
apply addHom_ext

Premises used: DirectSum.addHom_ext
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
H :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (ai + bi) : (a : A (ai + bi)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ax bx) : ⨁ (i : ι), A i)
    ((of A (bi + ai) : (a : A (bi + ai)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) bx ax) : ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A ai : (a : A ai) → ⨁ (i : ι), A i) ax) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A bi : (a : A bi) → ⨁ (i : ι), A i) bx) :
      ⨁ (i : ι), A i)
    ((((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A ai : (a : A ai) → ⨁ (i : ι), A i) ax) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A bi : (a : A bi) → ⨁ (i : ι), A i) bx) :
      ⨁ (i : ι), A i)

Tactic:
rw [AddMonoidHom.flip_apply, mulHom_of_of, mulHom_of_of]

Premises used: DirectSum.mulHom_of_of, AddMonoidHom.flip_apply
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (ai + bi) : (a : A (ai + bi)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ax bx) : ⨁ (i : ι), A i)
    ((of A (bi + ai) : (a : A (bi + ai)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) bx ax) : ⨁ (i : ι), A i)

Tactic:
of_eq_of_gradedMonoid_eq (GCommSemiring.mul_comm ⟨ai, ax⟩ ⟨bi, bx⟩)

Premises used: DirectSum.GCommSemiring.mul_comm, DirectSum.of_eq_of_gradedMonoid_eq, Sigma.mk
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (ai + bi) : (a : A (ai + bi)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) ax bx) : ⨁ (i : ι), A i)
    ((of A (bi + ai) : (a : A (bi + ai)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) bx ax) : ⨁ (i : ι), A i)

Tactic:
exact of_eq_of_gradedMonoid_eq (GCommSemiring.mul_comm ⟨ai, ax⟩ ⟨bi, bx⟩)

Premises used: DirectSum.GCommSemiring.mul_comm, DirectSum.of_eq_of_gradedMonoid_eq, Sigma.mk
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : Zero ι
inst_2 : GradedMonoid.GOne A
inst_3 : (i : ι) → AddCommMonoid (A i)
⊢ Eq (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : AddZeroClass ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
i : ι
a : A 0
b : A i
⊢ (of A i : (a : A i) → ⨁ (i : ι), A i) (a • b) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i)
      ((of A i : (a : A i) → ⨁ (i : ι), A i) b : ⨁ (i : ι), A i)

Tactic:
(of_eq_of_gradedMonoid_eq (GradedMonoid.mk_zero_smul a b)).trans (of_mul_of _ _).symm

Premises used: DirectSum.of_mul_of, GradedMonoid.mk_zero_smul, DirectSum.of_eq_of_gradedMonoid_eq, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : AddZeroClass ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
a b : A 0
⊢ (of A 0 : (a : A 0) → ⨁ (i : ι), A i) (a * b) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) b : ⨁ (i : ι), A i)

Tactic:
of_zero_smul A a b

Premises used: DirectSum.of_zero_smul
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : AddZeroClass ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
i : ι
this : SMulWithZero (A 0) (⨁ (i : ι), A i) :=
  SMulWithZero.compHom (⨁ (i : ι), A i) (↑(of A 0) : ZeroHom (A 0) (⨁ (i : ι), A i))
⊢ SMulWithZero (A 0) (A i)

Tactic:
exact Function.Injective.smulWithZero (of A i).toZeroHom DFinsupp.single_injective
    (of_zero_smul A)

Premises used: DirectSum.of_zero_smul, AddMonoidHom.toZeroHom, DFinsupp.single_injective, DirectSum.of, Function.Injective.smulWithZero
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
a : A 0
rw :
  (of A 0 : (a : A 0) → ⨁ (i : ι), A i) 1 =
    HPow.hPow (α := ⨁ (i : ι), A i) (β := ℕ) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) 0
rw₁ : Eq (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) 1) 1
rw₂ rw₃ : Eq (α := ⨁ (i : ι), A i) 1 1
⊢ (of A 0 : (a : A 0) → ⨁ (i : ι), A i) (HPow.hPow (β := ℕ) a 0) =
    HPow.hPow (α := ⨁ (i : ι), A i) (β := ℕ) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) 0

Tactic:
rw [pow_zero, pow_zero, DirectSum.of_zero_one]

Premises used: pow_zero, DirectSum.of_zero_one
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
a : A 0
n : ℕ
rw :
  (of A 0 : (a : A 0) → ⨁ (i : ι), A i) (a ^ n * a) =
    HPow.hPow (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) (n + 1)
rw₁ :
  (of A 0 : (a : A 0) → ⨁ (i : ι), A i) (a ^ n * a) =
    HMul.hMul (β := ⨁ (i : ι), A i)
      (HPow.hPow (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i)
rw₂ :
  HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (a ^ n) : ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) =
    HMul.hMul (β := ⨁ (i : ι), A i)
      (HPow.hPow (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i)
rw₃ rw₄ :
  HMul.hMul (β := ⨁ (i : ι), A i)
      (HPow.hPow (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) =
    HMul.hMul (β := ⨁ (i : ι), A i)
      (HPow.hPow (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i)
⊢ (of A 0 : (a : A 0) → ⨁ (i : ι), A i) (a ^ (n + 1)) =
    HPow.hPow (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) (n + 1)

Tactic:
rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]

Premises used: pow_succ, DirectSum.of_zero_mul
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
n : ℕ
⊢ Eq (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (↑n : A 0)) (↑n : ⨁ (i : ι), A i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
n : ℕ
inst_4 : n.AtLeastTwo
⊢ Eq (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
of_natCast A n

Premises used: DirectSum.of_natCast
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommGroup (A i)
inst_2 : AddMonoid ι
inst_3 : GRing A
n : ℤ
⊢ Eq (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (↑n : A 0)) (↑n : ⨁ (i : ι), A i)

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 G : (⨁ (i : ι), A i) →+* R
h :
  ∀ (i : ι),
    Eq (α := AddMonoidHom.{u_2, u_3} (A i) R) (AddMonoidHom.comp (↑F : (⨁ (i : ι), A i) →+ R) (of A i))
      (AddMonoidHom.comp (↑G : (⨁ (i : ι), A i) →+ R) (of A i))
⊢ F = G

Tactic:
RingHom.coe_addMonoidHom_injective <| DirectSum.addHom_ext' h

Premises used: DirectSum.addHom_ext', RingHom.coe_addMonoidHom_injective
-- 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 g : (⨁ (i : ι), A i) →+* R
h :
  ∀ (i : ι) (x : A i),
    Eq.{u_3 + 1} (α := R)
      ((f : (a : ⨁ (i : ι), A i) → R) ((of A i : (a : A i) → ⨁ (i : ι), A i) x : ⨁ (i : ι), A i) : R)
      ((g : (a : ⨁ (i : ι), A i) → R) ((of A i : (a : A i) → ⨁ (i : ι), A i) x : ⨁ (i : ι), A i) : R)
⊢ f = g

Tactic:
ringHom_ext' fun i => AddMonoidHom.ext <| h i

Premises used: DirectSum.ringHom_ext', AddMonoidHom.ext