S : Type ?u.8733
R : Type u_1
R₁ : Type ?u.8739
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x x' y : M
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
S : Type ?u.8733
R : Type u_1
R₁ : Type ?u.8739
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x x' y : M
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)
simp only [← add_assoc]
S : Type ?u.8733
R : Type u_1
R₁ : Type ?u.8739
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x x' y : M
⊢ f (x + x' + y) + f y + f x' + f y + f x = f (x + y) + f (x' + y) + f y + f (x + x') ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
S : Type ?u.8733
R : Type u_1
R₁ : Type ?u.8739
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x x' y : M
⊢ polar f (x + x') y = polar f x y + polar f x' y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
simp only [polar, sub_eq_iff_eq_add, eq_sub_iff_add_eq, sub_add_eq_add_sub, add_sub]
S : Type ?u.8733
R : Type u_1
R₁ : Type ?u.8739
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
S : Type ?u.8733
R : Type u_1
R₁ : Type ?u.8739
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x x' y : M
⊢ f (x + x' + y) + f y + f x' + f y + f x = f (x + y) + f (x' + y) + f y + f (x + x') ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
simp only [add_right_comm _ (f y) _, add_right_comm _ (f x') (f x)]
no goals
S : Type ?u.8733
R : Type u_1
R₁ : Type ?u.8739
M : Type u_2
inst✝² : Ring R
inst✝¹ : CommRing R₁
inst✝ : AddCommGroup M
f : M → R
x x' y : M
⊢ f (x + x' + y) + f x + f x' + f y + f y = f (x + y) + f (x' + y) + f (x + x') + f y ↔
    f (x + x' + y) + f x + f x' + f y = f (x + x') + f (x' + y) + f (y + x)
rw [add_comm y x, add_right_comm _ _ (f (x + y)), add_comm _ (f (x + y)),
  add_right_comm (f (x + y)), add_left_inj]