no goals
ι : Type u_1
R : Type ?u.79391
A : Type u_2
σ : Type u_3
inst✝⁷ : DecidableEq ι
inst✝⁶ : AddMonoid ι
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
a : ⨁ (i : ι), { x // x ∈ 𝒜 i }
i : ι
⊢ ↑(proj 𝒜 i) (↑(decompose 𝒜).symm a) = ↑(decompose 𝒜).symm (↑(of (fun i => (fun i => { x // x ∈ 𝒜 i }) i) i) (↑a i))
rw [GradedRing.proj_apply, decompose_symm_of, Equiv.apply_symm_apply]