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
inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (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)
have 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)
Tactic: dsimp only [DirectSum]
-- 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)
    ((((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)
have 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))
Tactic: rw [DFinsupp.sumAddHom_apply, AddMonoidHom.dfinsuppSum_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
inst_4 : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ 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))
have 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)
Tactic: apply congrArg _
-- 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 (α := (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)
have 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)
Tactic: funext x
-- 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 : 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))
⊢ a * b = b * a
have 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
Tactic: rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_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 : 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
⊢ a * b = b * a
have 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
Tactic: rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_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 : 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
⊢ a * b = b * a
have 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
Tactic: rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_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 : 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
⊢ a * b = b * a
have rw₃ : b * a = b * a
Tactic: rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_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 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ a * b = b * a
have suffices : Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) (mulHom A) (AddMonoidHom.flip (mulHom A))
Tactic: suffices mulHom A = (mulHom A).flip by
    rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_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 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ Eq (α := (⨁ (i : ι), A i) →+ (⨁ (i : ι), A i) →+ ⨁ (i : ι), A i) (mulHom A) (AddMonoidHom.flip (mulHom A))
have 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)
Tactic: apply addHom_ext
-- 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 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ 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)
have 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)
Tactic: apply addHom_ext
-- 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 : AddCommMonoid ι
inst_3 : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ 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)
have 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)
Tactic: rw [AddMonoidHom.flip_apply, mulHom_of_of, 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 : A 0
⊢ (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
have 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
Tactic: rw [pow_zero, pow_zero, DirectSum.of_zero_one]
-- 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 : 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
⊢ (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
have rw₁ : Eq (α := ⨁ (i : ι), A i) ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) 1) 1
Tactic: rw [pow_zero, pow_zero, DirectSum.of_zero_one]
-- 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 : 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
⊢ (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
have rw₂ : Eq (α := ⨁ (i : ι), A i) 1 1
Tactic: rw [pow_zero, pow_zero, DirectSum.of_zero_one]
-- 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 : A 0
n : ℕ
⊢ (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)
have 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)
Tactic: rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ 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
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)
⊢ (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)
have 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)
Tactic: rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ 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
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)
⊢ (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)
have 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)
Tactic: rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ 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
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)
⊢ (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)
have 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)
Tactic: rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]
-- Lean 4 proof step from Mathlib.Algebra.DirectSum.Ring (goal)
Goal:
ι : Type u_1
inst : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst_1 : (i : ι) → AddCommMonoid (A i)
inst_2 : AddMonoid ι
inst_3 : GSemiring A
inst_4 : Semiring R
f : (i : ι) → AddMonoidHom.{u_2, u_3} (A i) R
hone : Eq.{u_3 + 1} (α := R) ((f 0 : (a : A 0) → R) (GradedMonoid.GOne.one (A := A)) : R) (1 : R)
hmul :
  ∀ {i j : ι} (ai : A i) (aj : A j),
    (f (i + j) : (a : A (i + j)) → R) (GradedMonoid.GMul.mul (A := A) ai aj) =
      HMul.hMul (α := R) (β := R) ((f i : (a : A i) → R) ai : R) ((f j : (a : A j) → R) aj : R)
⊢ Eq.{u_3 + 1} (α := R) ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R) 1 : R) (1 : R)
have change : Eq.{u_3 + 1} (α := R)
  ((toAddMonoid (β := A) f : (a : ⨁ (i : ι), A i) → R)
      ((of A 0 : (a : A 0) → ⨁ (i : ι), A i) (GradedMonoid.GOne.one (A := A)) : ⨁ (i : ι), A i) :
    R)
  (1 : R)
Tactic: change (toAddMonoid f) (of _ 0 _) = 1