𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner (x + y) (x - y) = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner (x + y) (x - y) = 0 ↔ ‖x‖ = ‖y‖
conv_rhs => rw [← mul_self_inj_of_nonneg (norm_nonneg _) (norm_nonneg _)]
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner x x + inner y x = inner y x + inner y y ↔ inner x x = inner y y
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner (x + y) (x - y) = 0 ↔ ‖x‖ * ‖x‖ = ‖y‖ * ‖y‖
simp only [← @inner_self_eq_norm_mul_norm ℝ, inner_add_left, inner_sub_right, real_inner_comm y x,
  sub_eq_zero, re_to_real]
case mp
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner x x + inner y x = inner y x + inner y y → inner x x = inner y y

case mpr
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner x x = inner y y → inner x x + inner y x = inner y x + inner y y
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner x x + inner y x = inner y x + inner y y ↔ inner x x = inner y y
constructor
case mp
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
h : inner x x + inner y x = inner y x + inner y y
⊢ inner x x = inner y y
case mp
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner x x + inner y x = inner y x + inner y y → inner x x = inner y y
intro h
case mp
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
h : inner y x + inner x x = inner y x + inner y y
⊢ inner x x = inner y y
case mp
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
h : inner x x + inner y x = inner y x + inner y y
⊢ inner x x = inner y y
rw [add_comm] at h
no goals
case mp
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
h : inner y x + inner x x = inner y x + inner y y
⊢ inner x x = inner y y
linarith
case mpr
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
h : inner x x = inner y y
⊢ inner x x + inner y x = inner y x + inner y y
case mpr
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
⊢ inner x x = inner y y → inner x x + inner y x = inner y x + inner y y
intro h
no goals
case mpr
𝕜 : Type ?u.3117342
E : Type ?u.3117345
F : Type u_1
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
x y : F
h : inner x x = inner y y
⊢ inner x x + inner y x = inner y x + inner y y
linarith