case intro
ι : Type u_1
R : Type ?u.386108
A : Type u_2
σ : Type u_3
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = if i ≤ n then ↑(↑(↑(decompose 𝒜) a) (n - i)) * ↑b else 0
ι : Type u_1
R : Type ?u.386108
A : Type u_2
σ : Type u_3
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
b_mem : b ∈ 𝒜 i
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(↑(↑(decompose 𝒜) a) (n - i)) * b else 0
lift b to 𝒜 i using b_mem
no goals
case intro
ι : Type u_1
R : Type ?u.386108
A : Type u_2
σ : Type u_3
inst✝⁹ : Semiring A
inst✝⁸ : DecidableEq ι
inst✝⁷ : CanonicallyOrderedAddMonoid ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
n✝ i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n : ι
inst✝ : Decidable (i ≤ n)
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = if i ≤ n then ↑(↑(↑(decompose 𝒜) a) (n - i)) * ↑b else 0
rw [decompose_mul, decompose_coe, coe_mul_of_apply]