ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ ↑(smulAddMonoidHom A M) 1 = AddMonoidHom.id (⨁ (i : ι), M i)
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ 1 • x = x
suffices smulAddMonoidHom A M 1 = AddMonoidHom.id (⨁ i, M i) from FunLike.congr_fun this x
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ ∀ (i : ι) (y : M i),
    ↑(↑(smulAddMonoidHom A M) 1) (↑(of (fun i => M i) i) y) =
      ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) y)
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ ↑(smulAddMonoidHom A M) 1 = AddMonoidHom.id (⨁ (i : ι), M i)
apply DirectSum.addHom_ext
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(↑(smulAddMonoidHom A M) 1) (↑(of (fun i => M i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
⊢ ∀ (i : ι) (y : M i),
    ↑(↑(smulAddMonoidHom A M) 1) (↑(of (fun i => M i) i) y) =
      ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) y)
intro i xi
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(↑(smulAddMonoidHom A M) (↑(of A 0) GOne.one)) (↑(of (fun i => M i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(↑(smulAddMonoidHom A M) 1) (↑(of (fun i => M i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
rw [show (1 : DirectSum ι fun i => A i) = (of A 0) GOne.one by rfl]
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(of M (0 + i)) (GSmul.smul GOne.one xi) = ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(↑(smulAddMonoidHom A M) (↑(of A 0) GOne.one)) (↑(of (fun i => M i) i) xi) =
    ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
rw [smulAddMonoidHom_apply_of_of]
no goals
case H
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ ↑(of M (0 + i)) (GSmul.smul GOne.one xi) = ↑(AddMonoidHom.id (⨁ (i : ι), M i)) (↑(of (fun i => M i) i) xi)
exact DirectSum.of_eq_of_gradedMonoid_eq (one_smul (GradedMonoid A) <| GradedMonoid.mk i xi)
no goals
ι : Type u_1
A : ι → Type u_2
M : ι → Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : (i : ι) → AddCommMonoid (A i)
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : DecidableEq ι
inst✝¹ : GMonoid A
inst✝ : Gmodule A M
x : ⨁ (i : ι), M i
i : ι
xi : M i
⊢ 1 = ↑(of A 0) GOne.one
rfl