ι : 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)
ι : 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
suffices (mulHom A).flip One.one = AddMonoidHom.id (⨁ i, A i) from FunLike.congr_fun this x
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)
ι : 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)
apply addHom_ext
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)
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)
intro i xi
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)
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)
simp only [One.one]
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)
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)
rw [flip_apply, mulHom_of_of]
no goals
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)
exact of_eq_of_gradedMonoid_eq (mul_one <| GradedMonoid.mk i xi)