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

case h.inr
ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
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✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
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✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
⊢ ↑(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✝³ : (i : ι) → CanonicallyOrderedAddMonoid (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
f g : Π₀ (i : ι), α i
i : ι
a b : α i
inst✝ : DecidableEq ι
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]