awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
p : E
⊢ (K.reflection : (a : E) → E) p = HSMul.hSMul (α := ℕ) (β := E) 2 ((K.starProjection : (a : E) → E) p : E) - p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ K.reflection.symm = K.reflection

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearEquiv.ofInvolutive, Submodule.reflection, Submodule.reflectionLinearEquiv, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ K.reflection⁻¹ = K.reflection

Tactic:
rfl

Premises used: LinearEquiv.symm, LinearIsometryEquiv.symm, LinearEquiv.ofInvolutive, Submodule.reflection, Submodule.reflectionLinearEquiv, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
p : E
⊢ (K.reflection : (a : E) → E) ((K.reflection : (a : E) → E) p : E) = p

Tactic:
K.reflection.left_inv p

Premises used: LinearIsometryEquiv.toLinearEquiv, LinearEquiv.left_inv, Submodule.reflection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ Function.Involutive (α := E) (⇑K.reflection : (a : E) → E)

Tactic:
K.reflection_reflection

Premises used: Submodule.reflection_reflection, Function.Involutive
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ K.reflection.trans K.reflection = LinearIsometryEquiv.refl 𝕜 E

Tactic:
LinearIsometryEquiv.ext <| reflection_involutive K

Premises used: Submodule.reflection_involutive, LinearIsometryEquiv.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ K.reflection * K.reflection = 1

Tactic:
reflection_trans_reflection _

Premises used: Submodule.reflection_trans_reflection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
simp :
  HSMul.hSMul (α := ℕ) 2 (HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E)) - v =
    v - HSMul.hSMul (α := ℕ) (β := E) 2 ((K.starProjection : (a : E) → E) v : E)
⊢ Eq (α := E) ((Kᗮ.reflection : (a : E) → E) v : E) (-(K.reflection : (a : E) → E) v : E)

Tactic:
simp [reflection_apply]

Premises used: Submodule.reflection_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ HSMul.hSMul (α := ℕ) 2 (HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E)) - v =
    v - HSMul.hSMul (α := ℕ) (β := E) 2 ((K.starProjection : (a : E) → E) v : E)

Tactic:
abel
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
h :
  ∀ (x : E),
    Eq (α := E) ((Kᗮ.reflection : (a : E) → E) x : E)
      ((K.reflection.trans (LinearIsometryEquiv.neg 𝕜) : (a : E) → E) x : E)
⊢ Kᗮ.reflection = K.reflection.trans (LinearIsometryEquiv.neg 𝕜)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ Eq (α := E) ((Kᗮ.reflection : (a : E) → E) x : E)
    ((K.reflection.trans (LinearIsometryEquiv.neg 𝕜) : (a : E) → E) x : E)

Tactic:
apply reflection_orthogonal_apply

Premises used: Submodule.reflection_orthogonal_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
u v : E
rw :
  HSMul.hSMul (α := ℕ) (β := E) 2 ((starProjection (𝕜 ∙ u) : (a : E) → E) v : E) - v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
rw₁ :
  HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / (↑(HPow.hPow (β := ℕ) ‖u‖ 2) : 𝕜)) • u) - v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
rw₂ rw₃ :
  HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v
⊢ (reflection (𝕜 ∙ u) : (a : E) → E) v =
    HSMul.hSMul (α := ℕ) 2 ((⟪u, v⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖u‖ : 𝕜) 2) • u) - v

Tactic:
rw [reflection_apply, starProjection_singleton, ofReal_pow]

Premises used: Submodule.starProjection_singleton, Submodule.reflection_apply, RCLike.ofReal_pow
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
rw :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 2 ((K.starProjection : (a : E) → E) x : E) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 x ↔
    (K.starProjection : (a : E) → E) x = x
⊢ (K.reflection : (a : E) → E) x = x ↔ x ∈ K

Tactic:
rw [← starProjection_eq_self_iff, reflection_apply, sub_eq_iff_eq_add', ← two_smul 𝕜,
    two_smul ℕ, ← two_smul 𝕜]

Premises used: Submodule.reflection_apply, two_smul, Nat, sub_eq_iff_eq_add', Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 2 ((K.starProjection : (a : E) → E) x : E) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 x ↔
    (K.starProjection : (a : E) → E) x = x

Tactic:
(smul_right_injective E ?_).eq_iff

Premises used: Function.Injective.eq_iff, smul_right_injective
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
refine : Ne.{u_1 + 1} (α := 𝕜) 2 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) 2 ((K.starProjection : (a : E) → E) x : E) =
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2 x ↔
    (K.starProjection : (a : E) → E) x = x

Tactic:
refine (smul_right_injective E ?_).eq_iff

Premises used: Function.Injective.eq_iff, smul_right_injective
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ Ne.{u_1 + 1} (α := 𝕜) 2 0

Tactic:
two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ Ne.{u_1 + 1} (α := 𝕜) 2 0

Tactic:
exact two_ne_zero

Premises used: two_ne_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
hx : x ∈ K
⊢ (K.reflection : (a : E) → E) x = x

Tactic:
(reflection_eq_self_iff x).mpr hx

Premises used: Iff.mpr, Submodule.reflection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup E'
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x : E'
⊢ Eq (α := E') (((map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K).reflection : (a : E') → E') x : E')
    ((f : (a : E) → E') ((K.reflection : (a : E) → E) ((f.symm : (a : E') → E) x : E) : E) : E')

Tactic:
simp [reflection_apply, starProjection_map_apply f K x]

Premises used: Submodule.reflection_apply, Submodule.starProjection_map_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup E'
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
⊢ (map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K).reflection = f.symm.trans (K.reflection.trans f)

Tactic:
LinearIsometryEquiv.ext <| reflection_map_apply f K

Premises used: Submodule.reflection_map_apply, LinearIsometryEquiv.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
h : ∀ (x : E), Eq (α := E) ((reflection ⊥ : (a : E) → E) x : E) ((LinearIsometryEquiv.neg 𝕜 : (a : E) → E) x : E)
⊢ Eq.{u_2 + 1} (α := E ≃ₗᵢ[𝕜] E) (reflection ⊥) (LinearIsometryEquiv.neg 𝕜)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Eq (α := E) ((reflection ⊥ : (a : E) → E) x : E) ((LinearIsometryEquiv.neg 𝕜 : (a : E) → E) x : E)

Tactic:
simp [reflection_apply]

Premises used: Submodule.reflection_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
hv : v ∈ Kᗮ
⊢ (K.reflection : (a : E) → E) v = -v

Tactic:
simp [starProjection_apply, reflection_apply,
    orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hv]

Premises used: Submodule.reflection_apply, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.starProjection_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
hv : v ∈ K
⊢ (Kᗮ.reflection : (a : E) → E) v = -v

Tactic:
reflection_mem_subspace_orthogonalComplement_eq_neg (K.le_orthogonal_orthogonal hv)

Premises used: Submodule.le_orthogonal_orthogonal, Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : E
⊢ (reflection (𝕜 ∙ v)ᗮ : (a : E) → E) v = -v

Tactic:
reflection_mem_subspace_orthogonal_precomplement_eq_neg (Submodule.mem_span_singleton_self v)

Premises used: Submodule.reflection_mem_subspace_orthogonal_precomplement_eq_neg, Submodule.mem_span_singleton_self
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
set :
  let R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ;
  (R : (a : F) → F) v = w
⊢ (reflection (ℝ ∙ (v - w))ᗮ : (a : F) → F) v = w

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

Premises used: Real, HSub.hSub, Submodule.orthogonal, Submodule.span, Submodule.reflection, Singleton.singleton
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
this : HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
⊢ Ne (α := ℝ) 2 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
this : HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
a :
  Eq.{u_3 + 1} (α := F) ((fun (x : F) ↦ HSMul.hSMul (α := ℝ) 2 x) ((R : (a : F) → F) v))
    ((fun (x : F) ↦ HSMul.hSMul (α := ℝ) 2 x) w)
⊢ (R : (a : F) → F) v = w

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

Premises used: smul_right_injective
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
this : HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
⊢ Eq.{u_3 + 1} (α := F) ((fun (x : F) ↦ HSMul.hSMul (α := ℝ) 2 x) ((R : (a : F) → F) v))
    ((fun (x : F) ↦ HSMul.hSMul (α := ℝ) 2 x) w)

Tactic:
simpa [two_smul] using this

Premises used: two_smul
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
suffices : HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w
⊢ (R : (a : F) → F) v = w

Tactic:
suffices R v + R v = w + w by
    apply smul_right_injective F (by simp : (2 : ℝ) ≠ 0)
    simpa [two_smul] using this
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
⊢ (R : (a : F) → F) (v - w) = -(v - w)

Tactic:
have h₁ : R (v - w) = -(v - w) := reflection_orthogonalComplement_singleton_eq_neg (v - w)
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
hx : Membership.mem (γ := Submodule ℝ F) (ℝ ∙ (v - w))ᗮ (v + w)
⊢ (R : (a : F) → F) (v + w) = v + w

Tactic:
apply reflection_mem_subspace_eq_self

Premises used: Submodule.reflection_mem_subspace_eq_self
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
hx : inner ℝ (v + w) (v - w) = 0
⊢ Membership.mem (γ := Submodule ℝ F) (ℝ ∙ (v - w))ᗮ (v + w)

Tactic:
rw [Submodule.mem_orthogonal_singleton_iff_inner_left]

Premises used: Submodule.mem_orthogonal_singleton_iff_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
hx : ‖v‖ = ‖w‖
⊢ inner ℝ (v + w) (v - w) = 0

Tactic:
rw [real_inner_add_sub_eq_zero_iff]

Premises used: real_inner_add_sub_eq_zero_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
⊢ ‖v‖ = ‖w‖

Tactic:
h
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
⊢ ‖v‖ = ‖w‖

Tactic:
exact h
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
⊢ (R : (a : F) → F) (v + w) = v + 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
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
h₂ : (R : (a : F) → F) (v + w) = v + w
⊢ Eq.{u_3 + 1} (α := F) ((fun (x1 x2 : F) ↦ x1 + x2) ((R : (a : F) → F) (v + w)) ((R : (a : F) → F) (v - w)))
    ((fun (x1 x2 : F) ↦ x1 + x2) (v + w) (-(v - w)))

Tactic:
congr_arg₂ (· + ·) h₂ h₁

Premises used: HAdd.hAdd, congr_arg₂
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
h₂ : (R : (a : F) → F) (v + w) = v + w
h₃ :
  HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) =
    HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) (v + w) : F) ((R : (a : F) → F) (v - w) : F)
h₄ : w + w = v + w + -(v - w)
⊢ HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) = w + w

Tactic:
convert! congr_arg₂ (· + ·) h₂ h₁ using 1

Premises used: HAdd.hAdd, congr_arg₂
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
h₂ : (R : (a : F) → F) (v + w) = v + w
⊢ HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) v : F) ((R : (a : F) → F) v : F) =
    HAdd.hAdd (α := F) (β := F) ((R : (a : F) → F) (v + w) : F) ((R : (a : F) → F) (v - w) : F)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Goal:
F : Type u_3
inst : NormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
h : ‖v‖ = ‖w‖
R : F ≃ₗᵢ[ℝ] F := reflection (ℝ ∙ (v - w))ᗮ
h₁ : (R : (a : F) → F) (v - w) = -(v - w)
h₂ : (R : (a : F) → F) (v + w) = v + w
⊢ w + w = v + w + -(v - w)

Tactic:
abel
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst_3 : K₁.HasOrthogonalProjection
h₁ : ∀ (x : E), x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂
⊢ K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst_3 : K₁.HasOrthogonalProjection
x : E
h₁ : (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂
⊢ x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ ↔ x ∈ K₂

Tactic:
rw [Submodule.mem_sup]

Premises used: Submodule.mem_sup
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst_3 : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) x
⊢ x - (↑v : E) ∈ K₁ᗮ

Tactic:
have hvm : x - v ∈ K₁ᗮ := sub_starProjection_mem_orthogonal x
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst_3 : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) x
hvm : x - (↑v : E) ∈ K₁ᗮ
h₁ : (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) → x ∈ K₂
h₂ : x ∈ K₂ → ∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x
⊢ (∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x) ↔ x ∈ K₂

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst_3 : K₁.HasOrthogonalProjection
y : E
hy : y ∈ K₁
z : E
hz : z ∈ K₁ᗮ ⊓ K₂
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) (y + z)
hvm : y + z - (↑v : E) ∈ K₁ᗮ
⊢ y + z ∈ K₂

Tactic:
K₂.add_mem (h hy) hz.2

Premises used: And.right, Submodule.add_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst_3 : K₁.HasOrthogonalProjection
y : E
hy : y ∈ K₁
z : E
hz : z ∈ K₁ᗮ ⊓ K₂
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) (y + z)
hvm : y + z - (↑v : E) ∈ K₁ᗮ
⊢ y + z ∈ K₂

Tactic:
exact K₂.add_mem (h hy) hz.2

Premises used: And.right, Submodule.add_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst_3 : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) x
hvm : x - (↑v : E) ∈ K₁ᗮ
⊢ x ∈ K₂ → ∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x

Tactic:
fun hx => ⟨v, v.prop, x - v, ⟨hvm, K₂.sub_mem hx (h v.prop)⟩, add_sub_cancel _ _⟩

Premises used: HSub.hSub, add_sub_cancel, Subtype.prop, And.intro, Exists.intro, Subtype.val, Submodule.sub_mem
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
h : K₁ ≤ K₂
inst_3 : K₁.HasOrthogonalProjection
x : E
v : ↥K₁ := (K₁.orthogonalProjection : (a : E) → ↥K₁) x
hvm : x - (↑v : E) ∈ K₁ᗮ
⊢ x ∈ K₂ → ∃ y ∈ K₁, ∃ z ∈ K₁ᗮ ⊓ K₂, y + z = x

Tactic:
exact fun hx => ⟨v, v.prop, x - v, ⟨hvm, K₂.sub_mem hx (h v.prop)⟩, add_sub_cancel _ _⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ K ⊔ Kᗮ ⊓ ⊤ = ⊤

Tactic:
Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection (le_top : K ≤ ⊤)

Premises used: Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection, le_top
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
h : Kᗮ = Kᗮ ⊓ ⊤
⊢ K ⊔ Kᗮ = ⊤

Tactic:
convert! Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection (le_top : K ≤ ⊤) using 2

Premises used: Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection, le_top
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ Kᗮ = Kᗮ ⊓ ⊤

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
h : ∀ (v : E), v ∈ Kᗮᗮ ↔ v ∈ K
⊢ Kᗮᗮ = K

Tactic:
ext v