awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
N : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (N i)
inst_2 : (i : ι) → Module.{u_1, u_3} R (N i)
P : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (P i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (P i)
u : (i : ι) → AddEquiv.{u_3, u_4} (N i) (P i)
x : ⨁ (i : ι), N i
⊢ (map (α := P) (β := N) fun (i : ι) ↦ (u i).symm.toAddMonoidHom : (a : ⨁ (i : ι), P i) → ⨁ (i : ι), N i)
      (AddHom.toFun (↑(map (α := N) (β := P) fun (i : ι) ↦ (u i).toAddMonoidHom) : (⨁ (i : ι), N i) →ₙ+ ⨁ (i : ι), P i)
        x) =
    x

Tactic:
aesop
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
N : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (N i)
inst_2 : (i : ι) → Module.{u_1, u_3} R (N i)
P : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (P i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (P i)
u : (i : ι) → AddEquiv.{u_3, u_4} (N i) (P i)
y : ⨁ (i : ι), P i
⊢ AddHom.toFun (↑(map (α := N) (β := P) fun (i : ι) ↦ (u i).toAddMonoidHom) : (⨁ (i : ι), N i) →ₙ+ ⨁ (i : ι), P i)
      ((map (α := P) (β := N) fun (i : ι) ↦ (u i).symm.toAddMonoidHom : (a : ⨁ (i : ι), P i) → ⨁ (i : ι), N i) y) =
    y

Tactic:
aesop
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
ι : Type u_2
N : ι → Type u_3
inst : (i : ι) → AddCommMonoid (N i)
P : ι → Type u_4
inst_1 : (i : ι) → AddCommMonoid (P i)
u : (i : ι) → AddEquiv.{u_3, u_4} (N i) (P i)
⊢ Eq (α := (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
    (⇑(congrAddEquiv (N := N) (P := P) u).toAddMonoidHom : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
    (⇑(map (α := N) (β := P) fun (i : ι) ↦ (u i).toAddMonoidHom) : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i)

Tactic:
rfl

Premises used: DFinsupp.mapRange, DirectSum, rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
N : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (N i)
inst_2 : (i : ι) → Module.{u_1, u_3} R (N i)
P : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (P i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (P i)
u : (i : ι) → LinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id R) (N i) (P i)
r : R
x : ⨁ (i : ι), N i
⊢ Equiv.toFun (AddEquiv.toEquiv (congrAddEquiv (N := N) (P := P) fun (i : ι) ↦ (u i).toAddEquiv)) (r • x) =
    HSMul.hSMul (α := R) (β := ⨁ (i : ι), P i) ((RingHom.id R : (a : R) → R) r : R)
      (Equiv.toFun (AddEquiv.toEquiv (congrAddEquiv (N := N) (P := P) fun (i : ι) ↦ (u i).toAddEquiv)) x)

Tactic:
(DirectSum.lmap (fun i ↦ (u i).toLinearMap)).map_smul r x

Premises used: DirectSum.lmap, DFinsupp.mapRange, LinearEquiv.toLinearMap, LinearMap.map_smul
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
N : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (N i)
inst_2 : (i : ι) → Module.{u_1, u_3} R (N i)
P : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (P i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (P i)
u : (i : ι) → LinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id R) (N i) (P i)
r : R
x : ⨁ (i : ι), N i
⊢ Equiv.toFun (AddEquiv.toEquiv (congrAddEquiv (N := N) (P := P) fun (i : ι) ↦ (u i).toAddEquiv)) (r • x) =
    HSMul.hSMul (α := R) (β := ⨁ (i : ι), P i) ((RingHom.id R : (a : R) → R) r : R)
      (Equiv.toFun (AddEquiv.toEquiv (congrAddEquiv (N := N) (P := P) fun (i : ι) ↦ (u i).toAddEquiv)) x)

Tactic:
exact (DirectSum.lmap (fun i ↦ (u i).toLinearMap)).map_smul r x

Premises used: DirectSum.lmap, LinearEquiv.toLinearMap, LinearMap.map_smul
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
N : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (N i)
inst_2 : (i : ι) → Module.{u_1, u_3} R (N i)
P : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (P i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (P i)
u : (i : ι) → LinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id R) (N i) (P i)
⊢ Eq (α := (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
    (⇑(congrLinearEquiv (N := N) (P := P) u) : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
    (⇑(lmap (M := N) (N := P) fun (i : ι) ↦ (↑(u i) : N i →ₗ[R] P i)) : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i)

Tactic:
rfl

Premises used: DFinsupp.mapRange, DirectSum, rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
N : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (N i)
inst_2 : (i : ι) → Module.{u_1, u_3} R (N i)
P : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (P i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (P i)
u : (i : ι) → LinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id R) (N i) (P i)
⊢ (congrLinearEquiv (N := N) (P := P) u).toAddEquiv = congrAddEquiv (N := N) (P := P) fun (i : ι) ↦ (u i).toAddEquiv

Tactic:
rfl

Premises used: DirectSum.congrAddEquiv, rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_2
N : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (N i)
inst_2 : (i : ι) → Module.{u_1, u_3} R (N i)
P : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (P i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (P i)
u : (i : ι) → LinearEquiv.{u_1, u_1, u_3, u_4} (RingHom.id R) (N i) (P i)
⊢ (↑(congrLinearEquiv (N := N) (P := P) u) : (⨁ (i : ι), N i) →ₗ[R] ⨁ (i : ι), P i) =
    lmap (M := N) (N := P) fun (i : ι) ↦ (↑(u i) : N i →ₗ[R] P i)

Tactic:
rfl

Premises used: DirectSum.lmap, DFinsupp.mapRange.linearMap, DFinsupp.mapRange, DirectSum, rfl
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
i j : ι
a : A i
b : A j
h : GradedMonoid.mk (A := A) i a = GradedMonoid.mk (A := A) j b
⊢ Eq (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i)
    ((of A j : (a : A j) → ⨁ (i : ι), A i) b : ⨁ (i : ι), A i)

Tactic:
DFinsupp.single_eq_of_sigma_eq h

Premises used: DFinsupp.single, DFinsupp.single_eq_of_sigma_eq, DirectSum
-- 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) (1 : ⨁ (i : ι), A i)
    ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (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 : Add ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
x x_1 x_2 : ⨁ (i : ι), A i
⊢ x * (x_1 + x_2) = x * x_1 + x * x_2

Tactic:
simp only [Mul.mul, HMul.hMul, map_add]

Premises used: HMul.hMul, map_add, Mul.mul
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : Add ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
x x_1 x_2 : ⨁ (i : ι), A i
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2

Tactic:
simp only [Mul.mul, HMul.hMul, map_add, AddMonoidHom.add_apply]

Premises used: HMul.hMul, map_add, Mul.mul, AddMonoidHom.add_apply
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : Add ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
x : ⨁ (i : ι), A i
⊢ 0 * x = 0

Tactic:
simp only [Mul.mul, HMul.hMul, map_zero, AddMonoidHom.zero_apply]

Premises used: HMul.hMul, AddMonoidHom.zero_apply, map_zero, Mul.mul
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : Add ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
x : ⨁ (i : ι), A i
⊢ x * 0 = 0

Tactic:
simp only [Mul.mul, HMul.hMul, map_zero]

Premises used: HMul.hMul, map_zero, Mul.mul
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : Add ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
a b : ⨁ (i : ι), A i
⊢ (((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 =
    a * b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : Add ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ Eq (α := ⨁ (i : ι), A i)
    ((((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A i : (a : A i) → ⨁ (i : ι), A i) a) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A j : (a : A j) → ⨁ (i : ι), A i) b) :
      ⨁ (i : ι), A i)
    ((of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) a b) : ⨁ (i : ι), A i)

Tactic:
simp
-- Module: Mathlib.Algebra.DirectSum.Ring
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : Add ι
inst_2 : (i : ι) → AddCommMonoid (A i)
inst_3 : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i)
      ((of A j : (a : A j) → ⨁ (i : ι), A i) b : ⨁ (i : ι), A i) =
    (of A (i + j) : (a : A (i + j)) → ⨁ (i : ι), A i) (GradedMonoid.GMul.mul (A := A) a b)

Tactic:
mulHom_of_of a b

Premises used: DirectSum.mulHom_of_of
-- 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
x : ⨁ (i : ι), A i
suffices :
  Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one) (AddMonoidHom.id (⨁ (i : ι), A i))
⊢ 1 * x = x

Tactic:
suffices mulHom A One.one = AddMonoidHom.id (⨁ i, A i) from DFunLike.congr_fun this 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
x : ⨁ (i : ι), A i
H :
  ∀ (i : ι) (y : A i),
    Eq (α := ⨁ (i : ι), A i)
      (((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one :
            (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
          ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
        ⨁ (i : ι), A i)
      ((AddMonoidHom.id (⨁ (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) One.one) (AddMonoidHom.id (⨁ (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 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
H :
  Eq (α := ⨁ (i : ι), A i)
    ((((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A))) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    (((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)

Tactic:
simp only [One.one]

Premises used: One.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
x : ⨁ (i : ι), A i
i : ι
xi : A i
H :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (0 + i) : (a : A (0 + i)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (GradedMonoid.GOne.one (A := A)) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((((mulHom A : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A))) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)

Tactic:
rw [mulHom_of_of]

Premises used: DirectSum.mulHom_of_of
-- 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
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) (GradedMonoid.GOne.one (A := A)) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)

Tactic:
of_eq_of_gradedMonoid_eq (one_mul <| GradedMonoid.mk i xi)

Premises used: DFinsupp.single, DirectSum.of_eq_of_gradedMonoid_eq, one_mul, GradedMonoid.mk
-- 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
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) (GradedMonoid.GOne.one (A := A)) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)

Tactic:
exact of_eq_of_gradedMonoid_eq (one_mul <| GradedMonoid.mk i xi)
-- 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
x : ⨁ (i : ι), A i
suffices :
  Eq (α := (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
    ((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one)
    (AddMonoidHom.id (⨁ (i : ι), A i))
⊢ x * 1 = x

Tactic:
suffices (mulHom A).flip One.one = AddMonoidHom.id (⨁ i, A i) from DFunLike.congr_fun this 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
x : ⨁ (i : ι), A i
H :
  ∀ (i : ι) (y : A i),
    Eq (α := ⨁ (i : ι), A i)
      (((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one :
            (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
          ((of A i : (a : A i) → ⨁ (i : ι), A i) y) :
        ⨁ (i : ι), A i)
      ((AddMonoidHom.id (⨁ (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)
    ((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one)
    (AddMonoidHom.id (⨁ (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 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
H :
  Eq (α := ⨁ (i : ι), A i)
    ((((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A))) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    (((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) One.one :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)

Tactic:
simp only [One.one]

Premises used: One.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
x : ⨁ (i : ι), A i
i : ι
xi : A i
H :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (i + 0) : (a : A (i + 0)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) xi (GradedMonoid.GOne.one (A := A))) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((((AddMonoidHom.flip (mulHom A) : (a : ⨁ (i : ι), A i) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A))) :
            (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) :
          (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)

Tactic:
rw [flip_apply, 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 : AddMonoid ι
inst_3 : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (i + 0) : (a : A (i + 0)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) xi (GradedMonoid.GOne.one (A := A))) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)

Tactic:
of_eq_of_gradedMonoid_eq (mul_one <| GradedMonoid.mk i xi)

Premises used: DFinsupp.single, DirectSum.of_eq_of_gradedMonoid_eq, mul_one, GradedMonoid.mk
-- 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
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (i + 0) : (a : A (i + 0)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) xi (GradedMonoid.GOne.one (A := A))) :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.id (⨁ (i : ι), A i) : (a : ⨁ (i : ι), A i) → ⨁ (i : ι), A i)
        ((of A i : (a : A i) → ⨁ (i : ι), A i) xi) :
      ⨁ (i : ι), A i)

Tactic:
exact of_eq_of_gradedMonoid_eq (mul_one <| GradedMonoid.mk i xi)
-- 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 b c : ⨁ (i : ι), A i
this :
  Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) AddMonoidHom.mulLeft₃
    AddMonoidHom.mulRight₃
⊢ a * b * c = a * (b * c)

Tactic:
simpa only [AddMonoidHom.mulLeft₃_apply, AddMonoidHom.mulRight₃_apply] using
        DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c

Premises used: DFunLike.congr_fun, AddMonoidHom.mulLeft₃_apply, AddMonoidHom.mulRight₃_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
a b c : ⨁ (i : ι), A i
suffices :
  Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) AddMonoidHom.mulLeft₃
    AddMonoidHom.mulRight₃
⊢ a * b * c = a * (b * c)

Tactic:
suffices AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃ by
      simpa only [AddMonoidHom.mulLeft₃_apply, AddMonoidHom.mulRight₃_apply] using
        DFunLike.congr_fun (DFunLike.congr_fun (DFunLike.congr_fun this a) b) c
-- 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 b c : ⨁ (i : ι), A i
H :
  ∀ (ai : ι) (ax : A ai) (bi : ι) (bx : A bi) (ci : ι) (cx : A ci),
    Eq (α := ⨁ (i : ι), A i)
      ((AddMonoidHom.comp
              ((AddMonoidHom.comp
                    ((AddMonoidHom.comp AddMonoidHom.mulLeft₃ (of A ai) :
                        (a : A ai) → (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                      ax)
                    (of A bi) :
                  (a : A bi) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                bx)
              (of A ci) :
            (a : A ci) → ⨁ (i : ι), A i)
          cx :
        ⨁ (i : ι), A i)
      ((AddMonoidHom.comp
              ((AddMonoidHom.comp
                    ((AddMonoidHom.comp AddMonoidHom.mulRight₃ (of A ai) :
                        (a : A ai) → (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                      ax)
                    (of A bi) :
                  (a : A bi) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                bx)
              (of A ci) :
            (a : A ci) → ⨁ (i : ι), A i)
          cx :
        ⨁ (i : ι), A i)
⊢ Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) AddMonoidHom.mulLeft₃
    AddMonoidHom.mulRight₃

Tactic:
ext ai ax bi bx ci cx : 6
-- 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 b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
H :
  HMul.hMul (β := ⨁ (i : ι), A i)
      (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
        ((of A ai : (a : A ai) → ⨁ (i : ι), A i) ax : ⨁ (i : ι), A i)
        ((of A bi : (a : A bi) → ⨁ (i : ι), A i) bx : ⨁ (i : ι), A i))
      ((of A ci : (a : A ci) → ⨁ (i : ι), A i) cx : ⨁ (i : ι), A i) =
    HMul.hMul (α := ⨁ (i : ι), A i) ((of A ai : (a : A ai) → ⨁ (i : ι), A i) ax : ⨁ (i : ι), A i)
      (HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
        ((of A bi : (a : A bi) → ⨁ (i : ι), A i) bx : ⨁ (i : ι), A i)
        ((of A ci : (a : A ci) → ⨁ (i : ι), A i) cx : ⨁ (i : ι), A i))
⊢ Eq (α := ⨁ (i : ι), A i)
    ((AddMonoidHom.comp
            ((AddMonoidHom.comp
                  ((AddMonoidHom.comp AddMonoidHom.mulLeft₃ (of A ai) :
                      (a : A ai) → (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                    ax)
                  (of A bi) :
                (a : A bi) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              bx)
            (of A ci) :
          (a : A ci) → ⨁ (i : ι), A i)
        cx :
      ⨁ (i : ι), A i)
    ((AddMonoidHom.comp
            ((AddMonoidHom.comp
                  ((AddMonoidHom.comp AddMonoidHom.mulRight₃ (of A ai) :
                      (a : A ai) → (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
                    ax)
                  (of A bi) :
                (a : A bi) → (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i)
              bx)
            (of A ci) :
          (a : A ci) → ⨁ (i : ι), A i)
        cx :
      ⨁ (i : ι), A i)

Tactic:
dsimp only [coe_comp, Function.comp_apply, AddMonoidHom.mulLeft₃_apply,
    AddMonoidHom.mulRight₃_apply]

Premises used: AddMonoidHom.mulLeft₃_apply, AddMonoidHom.coe_comp, Function.comp_apply, AddMonoidHom.mulRight₃_apply