-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem reflection_sub {v w : F} (h : ‖v‖ = ‖w‖) : reflection (ℝ ∙ (v - w))ᗮ v = w

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
⊢ R v = w

Tactic:
suffices R v + R v = w + w by
  apply smul_right_injective F (by norm_num : (2 : ℝ) ≠ 0)
  simpa [two_smul] using this

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
⊢ R v + R v = w + w

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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

Tactic:
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

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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

Proof state:
case hx
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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})ᗮ

Tactic:
rw [Submodule.mem_orthogonal_singleton_iff_inner_left]

Result:
case hx
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : R (v - w) = -(v - w)
⊢ ⟪v + w, v - w⟫_ℝ = 0

Proof state:
case h.e'_3
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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)

Tactic:
abel

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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

Tactic:
apply reflection_mem_subspace_eq_self

Result:
case hx
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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})ᗮ

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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

Tactic:
apply smul_right_injective F (by norm_num : (2 : ℝ) ≠ 0)

Result:
case a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
this : R v + R v = w + w
⊢ (fun x => 2 • x) (R v) = (fun x => 2 • x) w

Proof state:
case hx
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : R (v - w) = -(v - w)
⊢ ‖v‖ = ‖w‖

Tactic:
exact h

Result:
no goals

Proof state:
case h.e'_2
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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)

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
⊢ (reflection (Submodule.span ℝ {v - w})ᗮ) v = w

Tactic:
set R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ v - w)ᗮ

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
⊢ R v = w

Proof state:
case hx
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : R (v - w) = -(v - w)
⊢ ⟪v + w, v - w⟫_ℝ = 0

Tactic:
rw [real_inner_add_sub_eq_zero_iff]

Result:
case hx
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
h₁ : R (v - w) = -(v - w)
⊢ ‖v‖ = ‖w‖

Proof state:
case a
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
this : R v + R v = w + w
⊢ (fun x => 2 • x) (R v) = (fun x => 2 • x) w

Tactic:
simpa [two_smul] using this

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
this : R v + R v = w + w
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (Submodule.span ℝ {v - w})ᗮ
⊢ R v + R v = w + w

Tactic:
have h₁ : R (v - w) = -(v - w) := reflection_orthogonalComplement_singleton_eq_neg (v - w)

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ 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