ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (-x) { val := i, property := H } else 0) = -if H : i ∈ s then x { val := i, property := H } else 0
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
⊢ ↑(mk s (-x)) i = ↑(-mk s x) i
simp only [neg_apply, mk_apply]
no goals
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
dec : DecidableEq ι
inst✝ : (i : ι) → AddGroup (β i)
s : Finset ι
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (-x) { val := i, property := H } else 0) = -if H : i ∈ s then x { val := i, property := H } else 0
split_ifs <;> [rfl; rw [neg_zero]]