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✝
f g : Π₀ (i : ι), α i
i : ι
⊢ ↑(f - g) i = (↑f - ↑g) i
ι : 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
f g : Π₀ (i : ι), α i
⊢ ↑(f - g) = ↑f - ↑g
ext i
no goals
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✝
f g : Π₀ (i : ι), α i
i : ι
⊢ ↑(f - g) i = (↑f - ↑g) i
exact tsub_apply f g i