no goals
𝕜 : Type u_1
E : Type ?u.600971
F : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : AddCommGroup F
inst✝ : Module 𝕜 F
c : Core 𝕜 F
x y z : F
⊢ inner (x - y) z = inner x z - inner y z
simp [sub_eq_add_neg, inner_add_left, inner_neg_left]