case h1
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddGroup α
k : ℕ
xs ys : List α
⊢ Sub.sub default default = default
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddGroup α
k : ℕ
xs ys : List α
⊢ get k (sub xs ys) = get k xs - get k ys
apply @get_pointwise _ _ _ ⟨0⟩ ⟨0⟩ ⟨0⟩
no goals
case h1
α✝ : Type u
β : Type v
γ : Type w
α : Type u
inst✝ : AddGroup α
k : ℕ
xs ys : List α
⊢ Sub.sub default default = default
apply sub_zero