𝕜 : Type ?u.2512953
E : Type u_1
F : Type ?u.2512959
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner (x + y) (x + y)) + ↑re (inner (x - y) (x - y)) = 2 * (↑re (inner x x) + ↑re (inner y y))
𝕜 : Type ?u.2512953
E : Type u_1
F : Type ?u.2512959
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ‖x + y‖ * ‖x + y‖ + ‖x - y‖ * ‖x - y‖ = 2 * (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
simp only [← @inner_self_eq_norm_mul_norm 𝕜]
𝕜 : Type ?u.2512953
E : Type u_1
F : Type ?u.2512959
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner x x + inner y y + (inner x x + inner y y)) =
    ↑re (inner x x) + ↑re (inner y y) + (↑re (inner x x) + ↑re (inner y y))
𝕜 : Type ?u.2512953
E : Type u_1
F : Type ?u.2512959
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner (x + y) (x + y)) + ↑re (inner (x - y) (x - y)) = 2 * (↑re (inner x x) + ↑re (inner y y))
rw [← re.map_add, parallelogram_law, two_mul, two_mul]
no goals
𝕜 : Type ?u.2512953
E : Type u_1
F : Type ?u.2512959
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : E
⊢ ↑re (inner x x + inner y y + (inner x x + inner y y)) =
    ↑re (inner x x) + ↑re (inner y y) + (↑re (inner x x) + ↑re (inner y y))
simp only [re.map_add]