𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
⊢ ↑R v = w
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
⊢ ↑(reflection (Submodule.span ℝ {v - w})ᗮ) v = w
set R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ v - w)ᗮ
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
⊢ ↑R v + ↑R v = w + w
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
⊢ ↑R v = w
suffices R v + R v = w + w by
  apply smul_right_injective F (by norm_num : (2 : ℝ) ≠ 0)
  simpa [two_smul] using this
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ ↑R v + ↑R v = w + w
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
⊢ ↑R v + ↑R v = w + w
have h₁ : R (v - w) = -(v - w) := reflection_orthogonalComplement_singleton_eq_neg (v - w)
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
h₂ : ↑R (v + w) = v + w
⊢ ↑R v + ↑R v = w + w
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ ↑R v + ↑R v = w + w
have h₂ : R (v + w) = v + w := by
  apply reflection_mem_subspace_eq_self
  rw [Submodule.mem_orthogonal_singleton_iff_inner_left]
  rw [real_inner_add_sub_eq_zero_iff]
  exact h
case a
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
this : ↑R v + ↑R v = w + w
⊢ (fun x x_1 => x • x_1) 2 (↑R v) = (fun x x_1 => x • x_1) 2 w
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
this : ↑R v + ↑R v = w + w
⊢ ↑R v = w
apply smul_right_injective F (by norm_num : (2 : ℝ) ≠ 0)
no goals
case a
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
this : ↑R v + ↑R v = w + w
⊢ (fun x x_1 => x • x_1) 2 (↑R v) = (fun x x_1 => x • x_1) 2 w
simpa [two_smul] using this
no goals
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
this : ↑R v + ↑R v = w + w
⊢ 2 ≠ 0
norm_num
case hx
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ v + w ∈ (Submodule.span ℝ {v - w})ᗮ
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ ↑R (v + w) = v + w
apply reflection_mem_subspace_eq_self
case hx
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ inner (v + w) (v - w) = 0
case hx
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ v + w ∈ (Submodule.span ℝ {v - w})ᗮ
rw [Submodule.mem_orthogonal_singleton_iff_inner_left]
case hx
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ ‖v‖ = ‖w‖
case hx
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ inner (v + w) (v - w) = 0
rw [real_inner_add_sub_eq_zero_iff]
no goals
case hx
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
⊢ ‖v‖ = ‖w‖
exact h
no goals
case h.e'_2
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
h₂ : ↑R (v + w) = v + w
⊢ ↑R v + ↑R v = ↑R (v + w) + ↑R (v - w)
simp
no goals
case h.e'_3
𝕜 : Type ?u.915894
E : Type ?u.915897
F : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst✝ : CompleteSpace F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : ↑R (v - w) = -(v - w)
h₂ : ↑R (v + w) = v + w
⊢ w + w = v + w + -(v - w)
abel