case intro
ι : Type u_3
R : Type ?u.367118
A : Type u_1
σ : Type u_2
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
h : i ≤ n
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = ↑(↑(↑(decompose 𝒜) a) (n - i)) * ↑b
ι : Type u_3
R : Type ?u.367118
A : Type u_1
σ : Type u_2
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
b_mem : b ∈ 𝒜 i
h : i ≤ n
⊢ ↑(↑(↑(decompose 𝒜) (a * b)) n) = ↑(↑(↑(decompose 𝒜) a) (n - i)) * b
lift b to 𝒜 i using b_mem
no goals
case intro
ι : Type u_3
R : Type ?u.367118
A : Type u_1
σ : Type u_2
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
h : i ≤ n
b : { x // x ∈ 𝒜 i }
⊢ ↑(↑(↑(decompose 𝒜) (a * ↑b)) n) = ↑(↑(↑(decompose 𝒜) a) (n - i)) * ↑b
rwa [decompose_mul, decompose_coe, coe_mul_of_apply_of_le]