case inl
ι : Type u_3
σ : Type u_2
S : Type ?u.448211
R : Type u_1
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' (n - i))

case inr
ι : Type u_3
σ : Type u_2
S : Type ?u.448211
R : Type u_1
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
ι : Type u_3
σ : Type u_2
S : Type ?u.448211
R : Type u_1
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = if i ≤ n then ↑r * ↑(↑r' (n - i)) else 0
split_ifs with h
no goals
case inl
ι : Type u_3
σ : Type u_2
S : Type ?u.448211
R : Type u_1
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = ↑r * ↑(↑r' (n - i))

case inr
ι : Type u_3
σ : Type u_2
S : Type ?u.448211
R : Type u_1
inst✝⁹ : DecidableEq ι
inst✝⁸ : Semiring R
inst✝⁷ : SetLike σ R
inst✝⁶ : AddSubmonoidClass σ R
A : ι → σ
inst✝⁵ : CanonicallyOrderedAddMonoid ι
inst✝⁴ : SetLike.GradedMonoid A
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
i : ι
r : { x // x ∈ A i }
r' : ⨁ (i : ι), { x // x ∈ A i }
n : ι
inst✝ : Decidable (i ≤ n)
h : ¬i ≤ n
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) r * r') n) = 0
exacts [coe_of_mul_apply_of_le _ _ _ n h, coe_of_mul_apply_of_not_le _ _ _ n h]