[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
src✝ : AddCommMonoid (⨁ (i : ι), A i) := inferInstance
x✝² x✝¹ x✝ : ⨁ (i : ι), A i
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝
[PROOFSTEP]
simp only [HMul.hMul, AddMonoidHom.map_add]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
src✝ : AddCommMonoid (⨁ (i : ι), A i) := inferInstance
x✝² x✝¹ x✝ : ⨁ (i : ι), A i
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝
[PROOFSTEP]
simp only [HMul.hMul, AddMonoidHom.map_add, AddMonoidHom.add_apply]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
src✝ : AddCommMonoid (⨁ (i : ι), A i) := inferInstance
x✝ : ⨁ (i : ι), A i
⊢ 0 * x✝ = 0
[PROOFSTEP]
simp only [HMul.hMul, map_zero, AddMonoidHom.zero_apply]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
src✝ : AddCommMonoid (⨁ (i : ι), A i) := inferInstance
x✝ : ⨁ (i : ι), A i
⊢ x✝ * 0 = 0
[PROOFSTEP]
simp only [HMul.hMul, AddMonoidHom.map_zero]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ↑(↑(mulHom A) (↑(of A i) a)) (↑(of A j) b) = ↑(of A (i + j)) (GradedMonoid.GMul.mul a b)
[PROOFSTEP]
unfold mulHom
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ↑(↑(toAddMonoid fun x =>
              AddMonoidHom.flip
                (toAddMonoid fun x_1 => AddMonoidHom.flip (AddMonoidHom.comp (↑compHom (of A (x + x_1))) (gMulHom A))))
          (↑(of A i) a))
      (↑(of A j) b) =
    ↑(of A (i + j)) (GradedMonoid.GMul.mul a b)
[PROOFSTEP]
simp only [toAddMonoid_of, flip_apply, coe_comp, Function.comp_apply]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : Add ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i j : ι
a : A i
b : A j
⊢ ↑(↑(↑compHom (of A (i + j))) (↑(gMulHom A) a)) b = ↑(of A (i + j)) (GradedMonoid.GMul.mul a b)
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ 1 * x = x
[PROOFSTEP]
suffices mulHom A One.one = AddMonoidHom.id (⨁ i, A i) from FunLike.congr_fun this x
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ↑(mulHom A) One.one = AddMonoidHom.id (⨁ (i : ι), A i)
[PROOFSTEP]
apply addHom_ext
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i),
    ↑(↑(mulHom A) One.one) (↑(of (fun i => A i) i) y) = ↑(AddMonoidHom.id (⨁ (i : ι), A i)) (↑(of (fun i => A i) i) y)
[PROOFSTEP]
intro i xi
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ↑(↑(mulHom A) One.one) (↑(of (fun i => A i) i) xi) = ↑(AddMonoidHom.id (⨁ (i : ι), A i)) (↑(of (fun i => A i) i) xi)
[PROOFSTEP]
simp only [One.one]
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ↑(↑(mulHom A) (↑(of (fun i => A i) 0) GradedMonoid.GOne.one)) (↑(of (fun i => A i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), A i)) (↑(of (fun i => A i) i) xi)
[PROOFSTEP]
rw [mulHom_of_of]
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ↑(of A (0 + i)) (GradedMonoid.GMul.mul GradedMonoid.GOne.one xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), A i)) (↑(of (fun i => A i) i) xi)
[PROOFSTEP]
exact of_eq_of_gradedMonoid_eq (one_mul <| GradedMonoid.mk i xi)
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ x * 1 = x
[PROOFSTEP]
suffices (mulHom A).flip One.one = AddMonoidHom.id (⨁ i, A i) from FunLike.congr_fun this x
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ↑(AddMonoidHom.flip (mulHom A)) One.one = AddMonoidHom.id (⨁ (i : ι), A i)
[PROOFSTEP]
apply addHom_ext
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i),
    ↑(↑(AddMonoidHom.flip (mulHom A)) One.one) (↑(of (fun i => A i) i) y) =
      ↑(AddMonoidHom.id (⨁ (i : ι), A i)) (↑(of (fun i => A i) i) y)
[PROOFSTEP]
intro i xi
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ↑(↑(AddMonoidHom.flip (mulHom A)) One.one) (↑(of (fun i => A i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), A i)) (↑(of (fun i => A i) i) xi)
[PROOFSTEP]
simp only [One.one]
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ↑(↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) 0) GradedMonoid.GOne.one)) (↑(of (fun i => A i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), A i)) (↑(of (fun i => A i) i) xi)
[PROOFSTEP]
rw [flip_apply, mulHom_of_of]
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
x : ⨁ (i : ι), A i
i : ι
xi : A i
⊢ ↑(of A (i + 0)) (GradedMonoid.GMul.mul xi GradedMonoid.GOne.one) =
    ↑(AddMonoidHom.id (⨁ (i : ι), A i)) (↑(of (fun i => A i) i) xi)
[PROOFSTEP]
exact of_eq_of_gradedMonoid_eq (mul_one <| GradedMonoid.mk i xi)
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
⊢ a * b * c = a * (b * c)
[PROOFSTEP]
suffices
  (mulHom A).compHom.comp (mulHom A) = (AddMonoidHom.compHom flipHom <| (mulHom A).flip.compHom.comp (mulHom A)).flip
  by
  have sol := FunLike.congr_fun (FunLike.congr_fun (FunLike.congr_fun this a) b) c
  have aux : ∀ a b, (mulHom A) a b = a * b := fun _ _ ↦ rfl
  simp only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, aux, flip_apply,
    AddMonoidHom.flipHom_apply] at sol
  exact sol
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
this :
  AddMonoidHom.comp (↑compHom (mulHom A)) (mulHom A) =
    AddMonoidHom.flip (↑(↑compHom flipHom) (AddMonoidHom.comp (↑compHom (AddMonoidHom.flip (mulHom A))) (mulHom A)))
⊢ a * b * c = a * (b * c)
[PROOFSTEP]
have sol := FunLike.congr_fun (FunLike.congr_fun (FunLike.congr_fun this a) b) c
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
this :
  AddMonoidHom.comp (↑compHom (mulHom A)) (mulHom A) =
    AddMonoidHom.flip (↑(↑compHom flipHom) (AddMonoidHom.comp (↑compHom (AddMonoidHom.flip (mulHom A))) (mulHom A)))
sol :
  ↑(↑(↑(AddMonoidHom.comp (↑compHom (mulHom A)) (mulHom A)) a) b) c =
    ↑(↑(↑(AddMonoidHom.flip
                  (↑(↑compHom flipHom) (AddMonoidHom.comp (↑compHom (AddMonoidHom.flip (mulHom A))) (mulHom A))))
              a)
          b)
      c
⊢ a * b * c = a * (b * c)
[PROOFSTEP]
have aux : ∀ a b, (mulHom A) a b = a * b := fun _ _ ↦ rfl
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
this :
  AddMonoidHom.comp (↑compHom (mulHom A)) (mulHom A) =
    AddMonoidHom.flip (↑(↑compHom flipHom) (AddMonoidHom.comp (↑compHom (AddMonoidHom.flip (mulHom A))) (mulHom A)))
sol :
  ↑(↑(↑(AddMonoidHom.comp (↑compHom (mulHom A)) (mulHom A)) a) b) c =
    ↑(↑(↑(AddMonoidHom.flip
                  (↑(↑compHom flipHom) (AddMonoidHom.comp (↑compHom (AddMonoidHom.flip (mulHom A))) (mulHom A))))
              a)
          b)
      c
aux : ∀ (a b : ⨁ (i : ι), A i), ↑(↑(mulHom A) a) b = a * b
⊢ a * b * c = a * (b * c)
[PROOFSTEP]
simp only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, aux, flip_apply,
  AddMonoidHom.flipHom_apply] at sol
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
this :
  AddMonoidHom.comp (↑compHom (mulHom A)) (mulHom A) =
    AddMonoidHom.flip (↑(↑compHom flipHom) (AddMonoidHom.comp (↑compHom (AddMonoidHom.flip (mulHom A))) (mulHom A)))
aux : ∀ (a b : ⨁ (i : ι), A i), ↑(↑(mulHom A) a) b = a * b
sol : a * b * c = a * (b * c)
⊢ a * b * c = a * (b * c)
[PROOFSTEP]
exact sol
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
⊢ AddMonoidHom.comp (↑compHom (mulHom A)) (mulHom A) =
    AddMonoidHom.flip (↑(↑compHom flipHom) (AddMonoidHom.comp (↑compHom (AddMonoidHom.flip (mulHom A))) (mulHom A)))
[PROOFSTEP]
ext ai ax bi bx ci cx
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp
                (↑(AddMonoidHom.comp (AddMonoidHom.comp (↑compHom (mulHom A)) (mulHom A)) (of (fun i => A i) ai)) ax)
                (of (fun i => A i) bi))
            bx)
          (of (fun i => A i) ci))
      cx =
    ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp
                (↑(AddMonoidHom.comp
                      (AddMonoidHom.flip
                        (↑(↑compHom flipHom) (AddMonoidHom.comp (↑compHom (AddMonoidHom.flip (mulHom A))) (mulHom A))))
                      (of (fun i => A i) ai))
                  ax)
                (of (fun i => A i) bi))
            bx)
          (of (fun i => A i) ci))
      cx
[PROOFSTEP]
dsimp only [coe_comp, Function.comp_apply, AddMonoidHom.compHom_apply_apply, flip_apply, AddMonoidHom.flipHom_apply]
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ ↑(↑(mulHom A) (↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx)))
      (↑(of (fun i => A i) ci) cx) =
    ↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax))
      (↑(↑(mulHom A) (↑(of (fun i => A i) bi) bx)) (↑(of (fun i => A i) ci) cx))
[PROOFSTEP]
simp_rw [mulHom_of_of]
[GOAL]
case H.h.H.h.H.h
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a b c : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
ci : ι
cx : A ci
⊢ ↑(of A (ai + bi + ci)) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul ax bx) cx) =
    ↑(of A (ai + (bi + ci))) (GradedMonoid.GMul.mul ax (GradedMonoid.GMul.mul bx cx))
[PROOFSTEP]
exact of_eq_of_gradedMonoid_eq (_root_.mul_assoc (GradedMonoid.mk ai ax) ⟨bi, bx⟩ ⟨ci, cx⟩)
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
src✝ : NonUnitalNonAssocSemiring (⨁ (i : ι), A i) := inferInstance
⊢ NatCast.natCast 0 = 0
[PROOFSTEP]
simp only [GSemiring.natCast_zero, map_zero]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
src✝ : NonUnitalNonAssocSemiring (⨁ (i : ι), A i) := inferInstance
n : ℕ
⊢ NatCast.natCast (n + 1) = NatCast.natCast n + 1
[PROOFSTEP]
simp_rw [GSemiring.natCast_succ]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
src✝ : NonUnitalNonAssocSemiring (⨁ (i : ι), A i) := inferInstance
n : ℕ
⊢ ↑(of (fun i => A i) 0) (GSemiring.natCast n + GradedMonoid.GOne.one) =
    ↑(of (fun i => A i) 0) (GSemiring.natCast n) + 1
[PROOFSTEP]
rw [map_add]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
src✝ : NonUnitalNonAssocSemiring (⨁ (i : ι), A i) := inferInstance
n : ℕ
⊢ ↑(of (fun i => A i) 0) (GSemiring.natCast n) + ↑(of (fun i => A i) 0) GradedMonoid.GOne.one =
    ↑(of (fun i => A i) 0) (GSemiring.natCast n) + 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
⊢ ↑(of A i) a ^ n = ↑(of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
[PROOFSTEP]
induction' n with n n_ih
[GOAL]
case zero
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
⊢ ↑(of A i) a ^ Nat.zero = ↑(of A (Nat.zero • i)) (GradedMonoid.GMonoid.gnpow Nat.zero a)
[PROOFSTEP]
exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm
[GOAL]
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : ↑(of A i) a ^ n = ↑(of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ ↑(of A i) a ^ Nat.succ n = ↑(of A (Nat.succ n • i)) (GradedMonoid.GMonoid.gnpow (Nat.succ n) a)
[PROOFSTEP]
rw [pow_succ, n_ih, of_mul_of a]
[GOAL]
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : ↑(of A i) a ^ n = ↑(of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ ↑(of A (i + n • i)) (GradedMonoid.GMul.mul a (GradedMonoid.GMonoid.gnpow n a)) =
    ↑(of A (Nat.succ n • i)) (GradedMonoid.GMonoid.gnpow (Nat.succ n) a)
[PROOFSTEP]
exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
l : List α
fι : α → ι
fA : (a : α) → A (fι a)
⊢ ↑(of A (List.dProdIndex l fι)) (List.dProd l fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) l)
[PROOFSTEP]
induction' l with head tail
[GOAL]
case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ ↑(of A (List.dProdIndex [] fι)) (List.dProd [] fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) [])
[PROOFSTEP]
simp only [List.map_nil, List.prod_nil, List.dProd_nil]
[GOAL]
case nil
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
⊢ ↑(of A (List.dProdIndex [] fι)) GradedMonoid.GOne.one = 1
[PROOFSTEP]
rfl
[GOAL]
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
tail_ih✝ :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (List.dProd (head :: tail) fι fA) =
    List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) (head :: tail))
[PROOFSTEP]
rename_i ih
[GOAL]
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (List.dProd (head :: tail) fι fA) =
    List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) (head :: tail))
[PROOFSTEP]
simp only [List.map_cons, List.prod_cons, List.dProd_cons, ← ih]
[GOAL]
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA)) =
    ↑(of A (fι head)) (fA head) * ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA)
[PROOFSTEP]
rw [DirectSum.of_mul_of (fA head)]
[GOAL]
case cons
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
α : Type u_3
fι : α → ι
fA : (a : α) → A (fι a)
head : α
tail : List α
ih :
  ↑(of A (List.dProdIndex tail fι)) (List.dProd tail fι fA) = List.prod (List.map (fun a => ↑(of A (fι a)) (fA a)) tail)
⊢ ↑(of A (List.dProdIndex (head :: tail) fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA)) =
    ↑(of A (fι head + List.dProdIndex tail fι)) (GradedMonoid.GMul.mul (fA head) (List.dProd tail fι fA))
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
n : ℕ
fι : Fin n → ι
fA : (a : Fin n) → A (fι a)
⊢ List.prod (List.ofFn fun a => ↑(of A (fι a)) (fA a)) =
    ↑(of A (List.dProdIndex (List.finRange n) fι)) (List.dProd (List.finRange n) fι fA)
[PROOFSTEP]
rw [List.ofFn_eq_map, ofList_dProd]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' = DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => ↑(of A (i + j)) (GradedMonoid.GMul.mul ai aj)
[PROOFSTEP]
change
  mulHom _ a a' =
    _
      -- Porting note: I have no idea how the proof from ml3 worked it used to be
        -- simpa only [mul_hom, to_add_monoid, dfinsupp.lift_add_hom_apply, dfinsupp.sum_add_hom_apply,
        -- add_monoid_hom.dfinsupp_sum_apply, flip_apply, add_monoid_hom.dfinsupp_sum_add_hom_apply],
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ ↑(↑(mulHom fun i => A i) a) a' =
    DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => ↑(of A (i + j)) (GradedMonoid.GMul.mul ai aj)
[PROOFSTEP]
rw [mulHom, toAddMonoid, DFinsupp.liftAddHom_apply, DFinsupp.sumAddHom_apply, AddMonoidHom.dfinsupp_sum_apply]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (DFinsupp.sum a fun a b =>
      ↑(↑(AddMonoidHom.flip
                (toAddMonoid fun x =>
                  AddMonoidHom.flip (AddMonoidHom.comp (↑compHom (of (fun i => A i) (a + x))) (gMulHom fun i => A i))))
            b)
        a') =
    DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => ↑(of A (i + j)) (GradedMonoid.GMul.mul ai aj)
[PROOFSTEP]
apply congrArg _
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ (fun a b =>
      ↑(↑(AddMonoidHom.flip
                (toAddMonoid fun x =>
                  AddMonoidHom.flip (AddMonoidHom.comp (↑compHom (of (fun i => A i) (a + x))) (gMulHom fun i => A i))))
            b)
        a') =
    fun i ai => DFinsupp.sum a' fun j aj => ↑(of A (i + j)) (GradedMonoid.GMul.mul ai aj)
[PROOFSTEP]
funext x
[GOAL]
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b =>
      ↑(↑(AddMonoidHom.flip
                (toAddMonoid fun x_1 =>
                  AddMonoidHom.flip
                    (AddMonoidHom.comp (↑compHom (of (fun i => A i) (x + x_1))) (gMulHom fun i => A i))))
            b)
        a') =
    fun ai => DFinsupp.sum a' fun j aj => ↑(of A (x + j)) (GradedMonoid.GMul.mul ai aj)
[PROOFSTEP]
simp_rw [flip_apply]
[GOAL]
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b =>
      ↑(↑(toAddMonoid fun x_1 =>
                AddMonoidHom.flip (AddMonoidHom.comp (↑compHom (of (fun i => A i) (x + x_1))) (gMulHom fun i => A i)))
            a')
        b) =
    fun ai => DFinsupp.sum a' fun j aj => ↑(of A (x + j)) (GradedMonoid.GMul.mul ai aj)
[PROOFSTEP]
erw [DFinsupp.sumAddHom_apply]
[GOAL]
case h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
x : ι
⊢ (fun b =>
      ↑(DFinsupp.sum a' fun x_1 =>
            ↑((fun x_2 =>
                  AddMonoidHom.flip (AddMonoidHom.comp (↑compHom (of (fun i => A i) (x + x_2))) (gMulHom fun i => A i)))
                x_1))
        b) =
    fun ai => DFinsupp.sum a' fun j aj => ↑(of A (x + j)) (GradedMonoid.GMul.mul ai aj)
[PROOFSTEP]
simp only [gMulHom, AddMonoidHom.dfinsupp_sum_apply, flip_apply, coe_comp, AddMonoidHom.coe_mk, ZeroHom.coe_mk,
  Function.comp_apply, AddMonoidHom.compHom_apply_apply]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)
a a' : ⨁ (i : ι), A i
⊢ a * a' =
    ∑ ij in DFinsupp.support a ×ˢ DFinsupp.support a',
      ↑(of (fun i => (fun i => A i) i) (ij.fst + ij.snd)) (GradedMonoid.GMul.mul (↑a ij.fst) (↑a' ij.snd))
[PROOFSTEP]
simp only [mul_eq_dfinsupp_sum, DFinsupp.sum, Finset.sum_product]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ a * b = b * a
[PROOFSTEP]
suffices mulHom A = (mulHom A).flip by rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_apply]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
this : mulHom A = AddMonoidHom.flip (mulHom A)
⊢ a * b = b * a
[PROOFSTEP]
rw [← mulHom_apply, this, AddMonoidHom.flip_apply, mulHom_apply]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ mulHom A = AddMonoidHom.flip (mulHom A)
[PROOFSTEP]
apply addHom_ext
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
⊢ ∀ (i : ι) (y : A i),
    ↑(mulHom A) (↑(of (fun i => A i) i) y) = ↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) i) y)
[PROOFSTEP]
intro ai ax
[GOAL]
case H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ↑(mulHom A) (↑(of (fun i => A i) ai) ax) = ↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)
[PROOFSTEP]
apply addHom_ext
[GOAL]
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
⊢ ∀ (i : ι) (y : A i),
    ↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) i) y) =
      ↑(↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) i) y)
[PROOFSTEP]
intro bi bx
[GOAL]
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ ↑(↑(mulHom A) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx) =
    ↑(↑(AddMonoidHom.flip (mulHom A)) (↑(of (fun i => A i) ai) ax)) (↑(of (fun i => A i) bi) bx)
[PROOFSTEP]
rw [AddMonoidHom.flip_apply, mulHom_of_of, mulHom_of_of]
[GOAL]
case H.H
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddCommMonoid ι
inst✝ : GCommSemiring A
a b : ⨁ (i : ι), A i
ai : ι
ax : A ai
bi : ι
bx : A bi
⊢ ↑(of A (ai + bi)) (GradedMonoid.GMul.mul ax bx) = ↑(of A (bi + ai)) (GradedMonoid.GMul.mul bx ax)
[PROOFSTEP]
exact of_eq_of_gradedMonoid_eq (GCommSemiring.mul_comm ⟨ai, ax⟩ ⟨bi, bx⟩)
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : AddZeroClass ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i : ι
⊢ SMulWithZero (A 0) (A i)
[PROOFSTEP]
letI := SMulWithZero.compHom (⨁ i, A i) (of A 0).toZeroHom
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : AddZeroClass ι
inst✝¹ : (i : ι) → AddCommMonoid (A i)
inst✝ : GNonUnitalNonAssocSemiring A
i : ι
this : SMulWithZero (A 0) (⨁ (i : ι), A i) := SMulWithZero.compHom (⨁ (i : ι), A i) ↑(of A 0)
⊢ SMulWithZero (A 0) (A i)
[PROOFSTEP]
exact Function.Injective.smulWithZero (of A i).toZeroHom DFinsupp.single_injective (of_zero_smul A)
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
⊢ ↑(of A 0) (a ^ 0) = ↑(of A 0) a ^ 0
[PROOFSTEP]
rw [pow_zero, pow_zero, DirectSum.of_zero_one]
  -- Porting note: Lean doesn't think this terminates if we only use `of_zero_pow` alone
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
a : A 0
n : ℕ
⊢ ↑(of A 0) (a ^ (n + 1)) = ↑(of A 0) a ^ (n + 1)
[PROOFSTEP]
rw [pow_succ, pow_succ, of_zero_mul, of_zero_pow _ n]
[GOAL]
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommGroup (A i)
inst✝¹ : AddMonoid ι
inst✝ : GRing A
n : ℤ
⊢ ↑(of A 0) ↑n = ↑n
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
⊢ ↑(toAddMonoid f) 1 = 1
[PROOFSTEP]
change (toAddMonoid f) (of _ 0 _) = 1
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
⊢ ↑(toAddMonoid f) (↑(of (fun i => A i) 0) GradedMonoid.GOne.one) = 1
[PROOFSTEP]
rw [toAddMonoid_of]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
⊢ ↑(f 0) GradedMonoid.GOne.one = 1
[PROOFSTEP]
exact hone
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
⊢ ∀ (x y : ⨁ (i : ι), A i),
    OneHom.toFun
        { toFun := ↑(toAddMonoid f),
          map_one' := (_ : ↑(toAddMonoid f) (↑(of (fun i => A i) 0) GradedMonoid.GOne.one) = 1) }
        (x * y) =
      OneHom.toFun
          { toFun := ↑(toAddMonoid f),
            map_one' := (_ : ↑(toAddMonoid f) (↑(of (fun i => A i) 0) GradedMonoid.GOne.one) = 1) }
          x *
        OneHom.toFun
          { toFun := ↑(toAddMonoid f),
            map_one' := (_ : ↑(toAddMonoid f) (↑(of (fun i => A i) 0) GradedMonoid.GOne.one) = 1) }
          y
[PROOFSTEP]
rw [(toAddMonoid f).map_mul_iff]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
⊢ AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid f) =
    AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid f)) (toAddMonoid f)
[PROOFSTEP]
refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
xi : ι
xv : A xi
⊢ ↑(AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid f)) (of (fun i => A i) xi)) xv =
    ↑(AddMonoidHom.comp (AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid f)) (toAddMonoid f))
          (of (fun i => A i) xi))
      xv
[PROOFSTEP]
refine DirectSum.addHom_ext' (fun yi ↦ AddMonoidHom.ext (fun yv ↦ ?_))
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp (AddMonoidHom.compr₂ AddMonoidHom.mul (toAddMonoid f)) (of (fun i => A i) xi)) xv)
          (of (fun i => A i) yi))
      yv =
    ↑(AddMonoidHom.comp
          (↑(AddMonoidHom.comp
                (AddMonoidHom.compl₂ (AddMonoidHom.comp AddMonoidHom.mul (toAddMonoid f)) (toAddMonoid f))
                (of (fun i => A i) xi))
            xv)
          (of (fun i => A i) yi))
      yv
[PROOFSTEP]
show toAddMonoid f (of A xi xv * of A yi yv) = toAddMonoid f (of A xi xv) * toAddMonoid f (of A yi yv)
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ ↑(toAddMonoid f) (↑(of A xi) xv * ↑(of A yi) yv) = ↑(toAddMonoid f) (↑(of A xi) xv) * ↑(toAddMonoid f) (↑(of A yi) yv)
[PROOFSTEP]
simp_rw [of_mul_of, toAddMonoid_of]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f : (i : ι) → A i →+ R
hone : ↑(f 0) GradedMonoid.GOne.one = 1
hmul : ∀ {i j : ι} (ai : A i) (aj : A j), ↑(f (i + j)) (GradedMonoid.GMul.mul ai aj) = ↑(f i) ai * ↑(f j) aj
src✝ : (⨁ (i : ι), A i) →+ R := toAddMonoid f
xi : ι
xv : A xi
yi : ι
yv : A yi
⊢ ↑(f (xi + yi)) (GradedMonoid.GMul.mul xv yv) = ↑(f xi) xv * ↑(f yi) yv
[PROOFSTEP]
exact hmul _ _
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ {i : ι} → A i →+ R
[PROOFSTEP]
intro i
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i : ι
⊢ A i →+ R
[PROOFSTEP]
exact (F : (⨁ i, A i) →+ R).comp (of _ i)
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ ↑(AddMonoidHom.comp (↑F) (of A 0)) GradedMonoid.GOne.one = 1
[PROOFSTEP]
simp only [AddMonoidHom.comp_apply]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ ↑↑F (↑(of A 0) GradedMonoid.GOne.one) = 1
[PROOFSTEP]
rw [← F.map_one]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ ↑↑F (↑(of A 0) GradedMonoid.GOne.one) = ↑F 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ ∀ {i j : ι} (ai : A i) (aj : A j),
    ↑(AddMonoidHom.comp (↑F) (of A (i + j))) (GradedMonoid.GMul.mul ai aj) =
      ↑(AddMonoidHom.comp (↑F) (of A i)) ai * ↑(AddMonoidHom.comp (↑F) (of A j)) aj
[PROOFSTEP]
intros i j ai aj
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
⊢ ↑(AddMonoidHom.comp (↑F) (of A (i + j))) (GradedMonoid.GMul.mul ai aj) =
    ↑(AddMonoidHom.comp (↑F) (of A i)) ai * ↑(AddMonoidHom.comp (↑F) (of A j)) aj
[PROOFSTEP]
simp [AddMonoidHom.comp_apply]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
i j : ι
ai : A i
aj : A j
⊢ ↑F (↑(of A (i + j)) (GradedMonoid.GMul.mul ai aj)) = ↑F (↑(of A i) ai) * ↑F (↑(of A j) aj)
[PROOFSTEP]
rw [← F.map_mul (of A i ai), of_mul_of ai]
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f :
  { f //
    ↑f GradedMonoid.GOne.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), ↑f (GradedMonoid.GMul.mul ai aj) = ↑f ai * ↑f aj }
⊢ (fun F =>
        { val := fun {i} => AddMonoidHom.comp (↑F) (of A i),
          property :=
            (_ :
              (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) GradedMonoid.GOne.one = 1 ∧
                ∀ {i j : ι} (ai : A i) (aj : A j),
                  (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) (GradedMonoid.GMul.mul ai aj) =
                    (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) ai *
                      (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) aj) })
      ((fun f =>
          toSemiring (fun x => ↑f) (_ : ↑↑f GradedMonoid.GOne.one = 1)
            (_ : ∀ {i j : ι} (ai : A i) (aj : A j), ↑↑f (GradedMonoid.GMul.mul ai aj) = ↑↑f ai * ↑↑f aj))
        f) =
    f
[PROOFSTEP]
ext xi xv
[GOAL]
case a.h.h
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
f :
  { f //
    ↑f GradedMonoid.GOne.one = 1 ∧ ∀ {i j : ι} (ai : A i) (aj : A j), ↑f (GradedMonoid.GMul.mul ai aj) = ↑f ai * ↑f aj }
xi : ι
xv : A xi
⊢ ↑↑((fun F =>
              { val := fun {i} => AddMonoidHom.comp (↑F) (of A i),
                property :=
                  (_ :
                    (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) GradedMonoid.GOne.one = 1 ∧
                      ∀ {i j : ι} (ai : A i) (aj : A j),
                        (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) (GradedMonoid.GMul.mul ai aj) =
                          (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) ai *
                            (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) aj) })
            ((fun f =>
                toSemiring (fun x => ↑f) (_ : ↑↑f GradedMonoid.GOne.one = 1)
                  (_ : ∀ {i j : ι} (ai : A i) (aj : A j), ↑↑f (GradedMonoid.GMul.mul ai aj) = ↑↑f ai * ↑↑f aj))
              f))
      xv =
    ↑↑f xv
[PROOFSTEP]
exact toAddMonoid_of (fun _ => f.1) xi xv
[GOAL]
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ (fun f =>
        toSemiring (fun x => ↑f) (_ : ↑↑f GradedMonoid.GOne.one = 1)
          (_ : ∀ {i j : ι} (ai : A i) (aj : A j), ↑↑f (GradedMonoid.GMul.mul ai aj) = ↑↑f ai * ↑↑f aj))
      ((fun F =>
          { val := fun {i} => AddMonoidHom.comp (↑F) (of A i),
            property :=
              (_ :
                (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) GradedMonoid.GOne.one = 1 ∧
                  ∀ {i j : ι} (ai : A i) (aj : A j),
                    (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) (GradedMonoid.GMul.mul ai aj) =
                      (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) ai *
                        (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) aj) })
        F) =
    F
[PROOFSTEP]
apply RingHom.coe_addMonoidHom_injective
[GOAL]
case a
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
⊢ (fun f => ↑f)
      ((fun f =>
          toSemiring (fun x => ↑f) (_ : ↑↑f GradedMonoid.GOne.one = 1)
            (_ : ∀ {i j : ι} (ai : A i) (aj : A j), ↑↑f (GradedMonoid.GMul.mul ai aj) = ↑↑f ai * ↑↑f aj))
        ((fun F =>
            { val := fun {i} => AddMonoidHom.comp (↑F) (of A i),
              property :=
                (_ :
                  (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) GradedMonoid.GOne.one = 1 ∧
                    ∀ {i j : ι} (ai : A i) (aj : A j),
                      (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) (GradedMonoid.GMul.mul ai aj) =
                        (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) ai *
                          (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) aj) })
          F)) =
    (fun f => ↑f) F
[PROOFSTEP]
refine DirectSum.addHom_ext' (fun xi ↦ AddMonoidHom.ext (fun xv ↦ ?_))
[GOAL]
case a
ι : Type u_1
inst✝⁴ : DecidableEq ι
A : ι → Type u_2
R : Type u_3
inst✝³ : (i : ι) → AddCommMonoid (A i)
inst✝² : AddMonoid ι
inst✝¹ : GSemiring A
inst✝ : Semiring R
F : (⨁ (i : ι), A i) →+* R
xi : ι
xv : A xi
⊢ ↑(AddMonoidHom.comp
          ((fun f => ↑f)
            ((fun f =>
                toSemiring (fun x => ↑f) (_ : ↑↑f GradedMonoid.GOne.one = 1)
                  (_ : ∀ {i j : ι} (ai : A i) (aj : A j), ↑↑f (GradedMonoid.GMul.mul ai aj) = ↑↑f ai * ↑↑f aj))
              ((fun F =>
                  { val := fun {i} => AddMonoidHom.comp (↑F) (of A i),
                    property :=
                      (_ :
                        (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) GradedMonoid.GOne.one = 1 ∧
                          ∀ {i j : ι} (ai : A i) (aj : A j),
                            (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) (GradedMonoid.GMul.mul ai aj) =
                              (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) ai *
                                (↑fun {i} => AddMonoidHom.comp (↑F) (of A i)) aj) })
                F)))
          (of (fun i => A i) xi))
      xv =
    ↑(AddMonoidHom.comp ((fun f => ↑f) F) (of (fun i => A i) xi)) xv
[PROOFSTEP]
simp only [RingHom.coe_addMonoidHom_mk, DirectSum.toAddMonoid_of, AddMonoidHom.mk_coe, AddMonoidHom.comp_apply,
  toSemiring_coe_addMonoidHom]
[GOAL]
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : AddMonoid ι
inst✝ : Semiring R
i j : ι
a b : R
⊢ ↑(of (fun x => R) i) a * ↑(of (fun i => R) j) b = ↑(of (fun i => R) (i + j)) (a * b)
[PROOFSTEP]
rw [DirectSum.of_mul_of, Mul.gMul_mul]


[GOAL]
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(↑(traceForm R L M) ⁅x, y⁆) z = ↑(↑(traceForm R L M) x) ⁅y, z⁆
[PROOFSTEP]
calc
  traceForm R L M ⁅x, y⁆ z = trace R _ (φ ⁅x, y⁆ ∘ₗ φ z) := by simp only [traceForm_apply_apply]
  _ = trace R _ ((φ x * φ y - φ y * φ x) * φ z) := ?_
  _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ y * (φ x * φ z)) := ?_
  _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ x * (φ z * φ y)) := ?_
  _ = traceForm R L M x ⁅y, z⁆ := ?_
[GOAL]
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(↑(traceForm R L M) ⁅x, y⁆) z = ↑(trace R M) (LinearMap.comp (↑φ ⁅x, y⁆) (↑φ z))
[PROOFSTEP]
simp only [traceForm_apply_apply]
[GOAL]
case calc_1
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(trace R M) (LinearMap.comp (↑φ ⁅x, y⁆) (↑φ z)) = ↑(trace R M) ((↑φ x * ↑φ y - ↑φ y * ↑φ x) * ↑φ z)
[PROOFSTEP]
simp only [LieHom.map_lie, Ring.lie_def, ← LinearMap.mul_eq_comp]
[GOAL]
case calc_2
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(trace R M) ((↑φ x * ↑φ y - ↑φ y * ↑φ x) * ↑φ z) =
    ↑(trace R M) (↑φ x * (↑φ y * ↑φ z)) - ↑(trace R M) (↑φ y * (↑φ x * ↑φ z))
[PROOFSTEP]
simp only [sub_mul, mul_sub, map_sub, mul_assoc]
[GOAL]
case calc_3
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(trace R M) (↑φ x * (↑φ y * ↑φ z)) - ↑(trace R M) (↑φ y * (↑φ x * ↑φ z)) =
    ↑(trace R M) (↑φ x * (↑φ y * ↑φ z)) - ↑(trace R M) (↑φ x * (↑φ z * ↑φ y))
[PROOFSTEP]
simp only [LinearMap.trace_mul_cycle' R (φ x) (φ z) (φ y)]
[GOAL]
case calc_4
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(trace R M) (↑φ x * (↑φ y * ↑φ z)) - ↑(trace R M) (↑φ x * (↑φ z * ↑φ y)) = ↑(↑(traceForm R L M) x) ⁅y, z⁆
[PROOFSTEP]
simp only [traceForm_apply_apply, LieHom.map_lie, Ring.lie_def, mul_sub, map_sub, ← LinearMap.mul_eq_comp]