case h
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
j : ι
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
⊢ single i (a - b) = single i a - single i b
ext j
case h.inl
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
⊢ ↑(single i (a - b)) i = ↑(single i a - single i b) i

case h.inr
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
j : ι
h : i ≠ j
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
case h
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
j : ι
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
obtain rfl | h := eq_or_ne i j
no goals
case h.inl
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
⊢ ↑(single i (a - b)) i = ↑(single i a - single i b) i
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
no goals
case h.inr
ι : Type u_1
α : Type u_2
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f g : ι →₀ α
i : ι
a b : α
j : ι
h : i ≠ j
⊢ ↑(single i (a - b)) j = ↑(single i a - single i b) j
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]