case inl
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i : ι
x : { x // x ∈ A i }
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) i) = ↑(if i = i then x else 0)

case inr
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : { x // x ∈ A i }
h : i ≠ j
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : { x // x ∈ A i }
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)
obtain rfl | h := Decidable.eq_or_ne i j
no goals
case inl
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i : ι
x : { x // x ∈ A i }
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) i) = ↑(if i = i then x else 0)
rw [DirectSum.of_eq_same, if_pos rfl]
no goals
case inr
ι : Type v
dec_ι : DecidableEq ι
β : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
γ : Type u₁
inst✝⁴ : AddCommMonoid γ
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
i j : ι
x : { x // x ∈ A i }
h : i ≠ j
⊢ ↑(↑(↑(of (fun i => { x // x ∈ A i }) i) x) j) = ↑(if i = j then x else 0)
rw [DirectSum.of_eq_of_ne _ _ _ _ h, if_neg h, ZeroMemClass.coe_zero, ZeroMemClass.coe_zero]