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
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
H :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (ai + bi + ci) : (a : A (ai + bi + ci)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (GradedMonoid.GMul.mul (A := A) ax bx) cx) :
      ⨁ (i : ι), A i)
    ((of A (ai + (bi + ci)) : (a : A (ai + (bi + ci))) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ax (GradedMonoid.GMul.mul (A := A) bx cx)) :
      ⨁ (i : ι), A i)
⊢ 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))

Tactic:
simp_rw [of_mul_of]

Premises used: DirectSum.of_mul_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
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (ai + bi + ci) : (a : A (ai + bi + ci)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (GradedMonoid.GMul.mul (A := A) ax bx) cx) :
      ⨁ (i : ι), A i)
    ((of A (ai + (bi + ci)) : (a : A (ai + (bi + ci))) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ax (GradedMonoid.GMul.mul (A := A) bx cx)) :
      ⨁ (i : ι), A i)

Tactic:
of_eq_of_gradedMonoid_eq (_root_.mul_assoc (GradedMonoid.mk ai ax) ⟨bi, bx⟩ ⟨ci, cx⟩)

Premises used: mul_assoc, DirectSum.of_eq_of_gradedMonoid_eq, Sigma.mk, 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
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (ai + bi + ci) : (a : A (ai + bi + ci)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (GradedMonoid.GMul.mul (A := A) ax bx) cx) :
      ⨁ (i : ι), A i)
    ((of A (ai + (bi + ci)) : (a : A (ai + (bi + ci))) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) ax (GradedMonoid.GMul.mul (A := A) bx cx)) :
      ⨁ (i : ι), A i)

Tactic:
exact of_eq_of_gradedMonoid_eq (_root_.mul_assoc (GradedMonoid.mk ai ax) ⟨bi, bx⟩ ⟨ci, cx⟩)

Premises used: mul_assoc, DirectSum.of_eq_of_gradedMonoid_eq, Sigma.mk, 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
⊢ Eq (α := ⨁ (i : ι), A i) (↑0) 0

Tactic:
simp only [NatCast.natCast, GSemiring.natCast_zero, map_zero]

Premises used: map_zero, NatCast.natCast, DirectSum.GSemiring.natCast_zero
-- 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 : ℕ
simp_rw :
  (of A 0 : (a : A 0) → ⨁ (i : ι), A i)
      (HAdd.hAdd (α := A 0) (@GSemiring.natCast _ A _ inst_1 _ n) (GradedMonoid.GOne.one (A := A))) =
    HAdd.hAdd (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (@GSemiring.natCast _ A _ inst_1 _ n) : ⨁ (i : ι), A i)
      (1 : ⨁ (i : ι), A i)
⊢ ↑(n + 1) = HAdd.hAdd (α := ⨁ (i : ι), A i) (↑n) 1

Tactic:
simp_rw [NatCast.natCast, GSemiring.natCast_succ]

Premises used: NatCast.natCast, DirectSum.GSemiring.natCast_succ
-- 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 : ℕ
rw :
  HAdd.hAdd (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (@GSemiring.natCast _ A _ inst_1 _ n) : ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) =
    HAdd.hAdd (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (@GSemiring.natCast _ A _ inst_1 _ n) : ⨁ (i : ι), A i)
      (1 : ⨁ (i : ι), A i)
⊢ (of A 0 : (a : A 0) → ⨁ (i : ι), A i)
      (HAdd.hAdd (α := A 0) (@GSemiring.natCast _ A _ inst_1 _ n) (GradedMonoid.GOne.one (A := A))) =
    HAdd.hAdd (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (@GSemiring.natCast _ A _ inst_1 _ n) : ⨁ (i : ι), A i)
      (1 : ⨁ (i : ι), A i)

Tactic:
rw [map_add]

Premises used: map_add
-- 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 : ℕ
⊢ HAdd.hAdd (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (@GSemiring.natCast _ A _ inst_1 _ n) : ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) =
    HAdd.hAdd (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (@GSemiring.natCast _ A _ inst_1 _ n) : ⨁ (i : ι), A i)
      (1 : ⨁ (i : ι), A i)

Tactic:
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
i : ι
a : A i
⊢ HPow.hPow (α := ⨁ (i : ι), A i) (β := ℕ) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) 0 =
    (of A (HSMul.hSMul (α := ℕ) 0 i) : (a : A (0 • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) 0 a)

Tactic:
of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm

Premises used: DFinsupp.single, npowRec, pow_zero, DirectSum.of_eq_of_gradedMonoid_eq, Eq.symm, 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
i : ι
a : A i
⊢ HPow.hPow (α := ⨁ (i : ι), A i) (β := ℕ) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) 0 =
    (of A (HSMul.hSMul (α := ℕ) 0 i) : (a : A (0 • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) 0 a)

Tactic:
exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm

Premises used: pow_zero, DirectSum.of_eq_of_gradedMonoid_eq, Eq.symm, 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
i : ι
a : A i
n : ℕ
n_ih :
  HPow.hPow (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n =
    (of A (n • i) : (a : A (n • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) n a)
succ :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (n • i + i) : (a : A (n • i + i)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (GradedMonoid.GMonoid.gnpow (A := A) n a) a) :
      ⨁ (i : ι), A i)
    ((of A ((n + 1) • i) : (a : A ((n + 1) • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) (n + 1) a) :
      ⨁ (i : ι), A i)
⊢ HPow.hPow (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) (n + 1) =
    (of A ((n + 1) • i) : (a : A ((n + 1) • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) (n + 1) a)

Tactic:
rw [pow_succ, n_ih, of_mul_of]

Premises used: pow_succ, DirectSum.of_mul_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
i : ι
a : A i
n : ℕ
n_ih :
  HPow.hPow (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n =
    (of A (n • i) : (a : A (n • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) n a)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (n • i + i) : (a : A (n • i + i)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (GradedMonoid.GMonoid.gnpow (A := A) n a) a) :
      ⨁ (i : ι), A i)
    ((of A ((n + 1) • i) : (a : A ((n + 1) • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) (n + 1) a) :
      ⨁ (i : ι), A i)

Tactic:
of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm

Premises used: pow_succ, DirectSum.of_eq_of_gradedMonoid_eq, Eq.symm, 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
i : ι
a : A i
n : ℕ
n_ih :
  HPow.hPow (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n =
    (of A (n • i) : (a : A (n • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) n a)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (n • i + i) : (a : A (n • i + i)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (GradedMonoid.GMonoid.gnpow (A := A) n a) a) :
      ⨁ (i : ι), A i)
    ((of A ((n + 1) • i) : (a : A ((n + 1) • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) (n + 1) a) :
      ⨁ (i : ι), A i)

Tactic:
exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm

Premises used: pow_succ, DirectSum.of_eq_of_gradedMonoid_eq, Eq.symm, 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
i : ι
a : A i
n : ℕ
zero :
  HPow.hPow (α := ⨁ (i : ι), A i) (β := ℕ) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) 0 =
    (of A (HSMul.hSMul (α := ℕ) 0 i) : (a : A (0 • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) 0 a)
succ :
  ∀ (n : ℕ)
    (n_ih :
      HPow.hPow (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n =
        (of A (n • i) : (a : A (n • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) n a)),
    HPow.hPow (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) (n + 1) =
      (of A ((n + 1) • i) : (a : A ((n + 1) • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) (n + 1) a)
⊢ HPow.hPow (α := ⨁ (i : ι), A i) ((of A i : (a : A i) → ⨁ (i : ι), A i) a : ⨁ (i : ι), A i) n =
    (of A (n • i) : (a : A (n • i)) → ⨁ (i : ι), A i) (GradedMonoid.GMonoid.gnpow (A := A) n a)

Tactic:
induction n with
  | zero => exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm
  | succ n n_ih =>
    rw [pow_succ, n_ih, of_mul_of]
    exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm

Premises used: pow_succ, DirectSum.of_mul_of, pow_zero, DirectSum.of_eq_of_gradedMonoid_eq, Eq.symm, 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
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
nil :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (List.dProdIndex [] fι) : (a : A ([].dProdIndex fι)) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) :
      ⨁ (i : ι), A i)
    (1 : ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (List.dProdIndex [] fι) : (a : A ([].dProdIndex fι)) → ⨁ (i : ι), A i) (List.dProd (A := A) [] fι fA) :
      ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) []) : ⨁ (i : ι), A i)

Tactic:
simp only [List.map_nil, List.prod_nil, List.dProd_nil]

Premises used: List.dProd_nil, List.prod_nil, List.map_nil
-- 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
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (List.dProdIndex [] fι) : (a : A ([].dProdIndex fι)) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) :
      ⨁ (i : ι), A i)
    (1 : ⨁ (i : ι), A i)

Tactic:
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
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (tail.dProdIndex fι) : (a : A (tail.dProdIndex fι)) → ⨁ (i : ι), A i) (tail.dProd (A := A) fι fA) :
      ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) tail) : ⨁ (i : ι), A i)
cons :
  (of A ((head :: tail).dProdIndex fι) : (a : A ((head :: tail).dProdIndex fι)) → ⨁ (i : ι), A i)
      (GradedMonoid.GMul.mul (A := A) (fA head) (tail.dProd (A := A) fι fA)) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A (fι head) : (a : A (fι head)) → ⨁ (i : ι), A i) (fA head) : ⨁ (i : ι), A i)
      ((of A (tail.dProdIndex fι) : (a : A (tail.dProdIndex fι)) → ⨁ (i : ι), A i) (tail.dProd (A := A) fι fA) :
        ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A ((head :: tail).dProdIndex fι) : (a : A ((head :: tail).dProdIndex fι)) → ⨁ (i : ι), A i)
        ((head :: tail).dProd (A := A) fι fA) :
      ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) (head :: tail)) :
      ⨁ (i : ι), A i)

Tactic:
simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]

Premises used: List.map_cons, List.dProd_cons, List.prod_cons
-- 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
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (tail.dProdIndex fι) : (a : A (tail.dProdIndex fι)) → ⨁ (i : ι), A i) (tail.dProd (A := A) fι fA) :
      ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) tail) : ⨁ (i : ι), A i)
cons :
  Eq (α := ⨁ (i : ι), A i)
    ((of A ((head :: tail).dProdIndex fι) : (a : A ((head :: tail).dProdIndex fι)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (fA head) (tail.dProd (A := A) fι fA)) :
      ⨁ (i : ι), A i)
    ((of A (fι head + tail.dProdIndex fι) : (a : A (fι head + tail.dProdIndex fι)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (fA head) (tail.dProd (A := A) fι fA)) :
      ⨁ (i : ι), A i)
⊢ (of A ((head :: tail).dProdIndex fι) : (a : A ((head :: tail).dProdIndex fι)) → ⨁ (i : ι), A i)
      (GradedMonoid.GMul.mul (A := A) (fA head) (tail.dProd (A := A) fι fA)) =
    HMul.hMul (α := ⨁ (i : ι), A i) (β := ⨁ (i : ι), A i)
      ((of A (fι head) : (a : A (fι head)) → ⨁ (i : ι), A i) (fA head) : ⨁ (i : ι), A i)
      ((of A (tail.dProdIndex fι) : (a : A (tail.dProdIndex fι)) → ⨁ (i : ι), A i) (tail.dProd (A := A) fι fA) :
        ⨁ (i : ι), A i)

Tactic:
rw [DirectSum.of_mul_of (fA head)]

Premises used: DirectSum.of_mul_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
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (tail.dProdIndex fι) : (a : A (tail.dProdIndex fι)) → ⨁ (i : ι), A i) (tail.dProd (A := A) fι fA) :
      ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) tail) : ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A ((head :: tail).dProdIndex fι) : (a : A ((head :: tail).dProdIndex fι)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (fA head) (tail.dProd (A := A) fι fA)) :
      ⨁ (i : ι), A i)
    ((of A (fι head + tail.dProdIndex fι) : (a : A (fι head + tail.dProdIndex fι)) → ⨁ (i : ι), A i)
        (GradedMonoid.GMul.mul (A := A) (fA head) (tail.dProd (A := A) fι fA)) :
      ⨁ (i : ι), A i)

Tactic:
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
α : Type u_3
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
nil :
  Eq (α := ⨁ (i : ι), A i)
    ((of A (List.dProdIndex [] fι) : (a : A ([].dProdIndex fι)) → ⨁ (i : ι), A i) (List.dProd (A := A) [] fι fA) :
      ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) []) : ⨁ (i : ι), A i)
cons :
  ∀ (head : α) (tail : List α),
    Eq (α := ⨁ (i : ι), A i)
        ((of A (tail.dProdIndex fι) : (a : A (tail.dProdIndex fι)) → ⨁ (i : ι), A i) (tail.dProd (A := A) fι fA) :
          ⨁ (i : ι), A i)
        (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) tail) :
          ⨁ (i : ι), A i) →
      Eq (α := ⨁ (i : ι), A i)
        ((of A ((head :: tail).dProdIndex fι) : (a : A ((head :: tail).dProdIndex fι)) → ⨁ (i : ι), A i)
            ((head :: tail).dProd (A := A) fι fA) :
          ⨁ (i : ι), A i)
        (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) (head :: tail)) :
          ⨁ (i : ι), A i)
⊢ Eq (α := ⨁ (i : ι), A i)
    ((of A (l.dProdIndex fι) : (a : A (l.dProdIndex fι)) → ⨁ (i : ι), A i) (l.dProd (A := A) fι fA) : ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : α) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) l) : ⨁ (i : ι), A i)

Tactic:
induction l with
  | nil => simp only [List.map_nil, List.prod_nil, List.dProd_nil]; rfl
  | cons head tail =>
    rename_i ih
    simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
    rw [DirectSum.of_mul_of (fA head)]
    rfl

Premises used: List.map_cons, List.dProd_nil, List.dProd_cons, List.prod_nil, List.prod_cons, List.map_nil
-- 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 : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
rw :
  Eq (α := ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : Fin n) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) (List.finRange n)) :
      ⨁ (i : ι), A i)
    ((of A ((List.finRange n).dProdIndex fι) : (a : A ((List.finRange n).dProdIndex fι)) → ⨁ (i : ι), A i)
        ((List.finRange n).dProd (A := A) fι fA) :
      ⨁ (i : ι), A i)
rw₁ rw₂ :
  Eq (α := ⨁ (i : ι), A i)
    (List.prod (List.map (fun (a : Fin n) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) (List.finRange n)))
    (List.prod (List.map (fun (a : Fin n) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) (List.finRange n)))
⊢ Eq (α := ⨁ (i : ι), A i)
    (List.prod (List.ofFn (n := n) fun (a : Fin n) ↦ (of A (fι a) : (a : A (fι a)) → ⨁ (i : ι), A i) (fA a)) :
      ⨁ (i : ι), A i)
    ((of A ((List.finRange n).dProdIndex fι) : (a : A ((List.finRange n).dProdIndex fι)) → ⨁ (i : ι), A i)
        ((List.finRange n).dProd (A := A) fι fA) :
      ⨁ (i : ι), A i)

Tactic:
rw [List.ofFn_eq_map, ofList_dProd]

Premises used: DirectSum.ofList_dProd, List.ofFn_eq_map
-- 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
change :
  Eq (α := ⨁ (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)
        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)
⊢ a * 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:
change mulHom _ a a' = _

Premises used: DFunLike.coe, DirectSum.mulHom
-- 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.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)
    ((((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)
        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 [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply]

Premises used: DFinsupp.liftAddHom_apply, DirectSum.mulHom, DirectSum.toAddMonoid