awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
    ((((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)
have 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)
Tactic: rw [flip_apply, mulHom_of_of]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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
⊢ a * b * c = a * (b * c)
have suffices : Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) AddMonoidHom.mulLeft₃
  AddMonoidHom.mulRight₃
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
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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
⊢ Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) AddMonoidHom.mulLeft₃
    AddMonoidHom.mulRight₃
have 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)
Tactic: ext ai ax bi bx ci cx : 6
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
    ((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)
have 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))
Tactic: dsimp only [coe_comp, Function.comp_apply, AddMonoidHom.mulLeft₃_apply,
    AddMonoidHom.mulRight₃_apply]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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
⊢ 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))
have 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)
Tactic: simp_rw [of_mul_of]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
n : ℕ
⊢ ↑(n + 1) = HAdd.hAdd (α := ⨁ (i : ι), A i) (↑n) 1
have 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)
Tactic: simp_rw [NatCast.natCast, GSemiring.natCast_succ]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
n : ℕ
⊢ (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)
have 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)
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ, n_ih, of_mul_of]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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 : ℕ
⊢ 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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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) (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)
have 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)
Tactic: simp only [List.map_nil, List.prod_nil, List.dProd_nil]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
        ((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)
have 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)
Tactic: simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
⊢ (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)
have 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)
Tactic: rw [DirectSum.of_mul_of (fA head)]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
⊢ 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)
have 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)
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
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
⊢ 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)
have 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)
Tactic: rw [List.ofFn_eq_map, ofList_dProd]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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)
⊢ 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)
have 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)))
Tactic: rw [List.ofFn_eq_map, ofList_dProd]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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' =
    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)
have 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)
Tactic: change mulHom _ a a' = _
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
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
⊢ 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)
have 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)
Tactic: rw [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply]