simp_rw [VIntegral, integral_symm y₁ y₂, smul_neg, neg_neg]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
z w p c A : ℂ
x x₁ x₂ y y₁ y₂ σ : ℝ
⊢ VIntegral f x y₁ y₂ = -VIntegral f x y₂ y₁
no goals