awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
⊢ Eq (α := ↥Kᗮ) ((Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) v : ↥Kᗮ) (0 : ↥Kᗮ)

Tactic:
orthogonalProjection_orthogonal_apply_eq_zero hv

Premises used: Submodule.orthogonalProjection_orthogonal_apply_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
⊢ Eq (α := ↥Kᗮ) ((Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) v : ↥Kᗮ) (0 : ↥Kᗮ)

Tactic:
exact orthogonalProjection_orthogonal_apply_eq_zero hv

Premises used: Submodule.orthogonalProjection_orthogonal_apply_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
h : U ≤ V
x : E
⊢ Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) x : ↥U)
    ((U.orthogonalProjection : (a : E) → ↥U) ((V.starProjection : (a : E) → E) x) : ↥U)

Tactic:
simpa only [sub_eq_zero, map_sub] using
      orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero
        (Submodule.orthogonal_le h (sub_starProjection_mem_orthogonal x))

Premises used: map_sub, sub_eq_zero, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.sub_starProjection_mem_orthogonal, Submodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
h : U ≤ V
x : E
nth_rw :
  Eq (α := E) (((U.subtypeL ∘SL U.orthogonalProjection) ∘SL V.starProjection : (a : E) → E) x : E)
    ((U.starProjection : (a : E) → E) x : E)
⊢ Eq (α := E) ((U.starProjection ∘SL V.starProjection : (a : E) → E) x : E) ((U.starProjection : (a : E) → E) x : E)

Tactic:
nth_rw 1 [starProjection]

Premises used: Submodule.starProjection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
h : U ≤ V
x : E
⊢ Eq (α := E) (((U.subtypeL ∘SL U.orthogonalProjection) ∘SL V.starProjection : (a : E) → E) x : E)
    ((U.starProjection : (a : E) → E) x : E)

Tactic:
simp [orthogonalProjection_starProjection_of_le h]

Premises used: Submodule.orthogonalProjection_starProjection_of_le
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ (↑p : E →ₗ[𝕜] E).range.HasOrthogonalProjection

Tactic:
have := hp.isClosed_range.completeSpace_coe
  .ofCompleteSpace _

Premises used: Submodule.HasOrthogonalProjection.ofCompleteSpace, LinearMap.range, ContinuousLinearMap.toLinearMap, IsClosed.completeSpace_coe
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
v : E
⊢ Membership.mem (α := E) p.range ((p : (a : E) → E) v : E) ∧ HSub.hSub (β := E) v ((p : (a : E) → E) v : E) ∈ p.rangeᗮ

Tactic:
simp [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric,
      ← Module.End.mul_apply, hp.isIdempotentElem.eq]

Premises used: LinearMap.IsSymmetricProjection.isIdempotentElem, LinearMap.IsSymmetricProjection.isSymmetric, LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range, Iff.mp, IsIdempotentElem.eq, Module.End.mul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : E
⊢ Eq (α := ↥(𝕜 ∙ v)ᗮ) ((orthogonalProjection (𝕜 ∙ v)ᗮ : (a : E) → ↥(𝕜 ∙ v)ᗮ) v : ↥(𝕜 ∙ v)ᗮ) (0 : ↥(𝕜 ∙ v)ᗮ)

Tactic:
orthogonalProjection_orthogonal_apply_eq_zero
    (Submodule.mem_span_singleton_self v)

Premises used: Submodule.mem_span_singleton_self, Submodule.orthogonalProjection_orthogonal_apply_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : E
rw : Eq (α := ↥(𝕜 ∙ v)ᗮ) ((orthogonalProjection (𝕜 ∙ v)ᗮ : (a : E) → ↥(𝕜 ∙ v)ᗮ) v : ↥(𝕜 ∙ v)ᗮ) (0 : ↥(𝕜 ∙ v)ᗮ)
⊢ Eq (α := E) ((starProjection (𝕜 ∙ v)ᗮ : (a : E) → E) v : E) (0 : E)

Tactic:
rw [starProjection_apply, coe_eq_zero]

Premises used: Submodule.starProjection_apply, Submodule.coe_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : E
⊢ Eq (α := ↥(𝕜 ∙ v)ᗮ) ((orthogonalProjection (𝕜 ∙ v)ᗮ : (a : E) → ↥(𝕜 ∙ v)ᗮ) v : ↥(𝕜 ∙ v)ᗮ) (0 : ↥(𝕜 ∙ v)ᗮ)

Tactic:
orthogonalProjection_orthogonalComplement_singleton_eq_zero v

Premises used: Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v : E
⊢ Eq (α := ↥(𝕜 ∙ v)ᗮ) ((orthogonalProjection (𝕜 ∙ v)ᗮ : (a : E) → ↥(𝕜 ∙ v)ᗮ) v : ↥(𝕜 ∙ v)ᗮ) (0 : ↥(𝕜 ∙ v)ᗮ)

Tactic:
exact orthogonalProjection_orthogonalComplement_singleton_eq_zero v

Premises used: Submodule.orthogonalProjection_orthogonalComplement_singleton_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
w : E
⊢ HAdd.hAdd (α := E) (β := E) ((K.starProjection : (a : E) → E) w : E) ((Kᗮ.starProjection : (a : E) → E) w : E) = w

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst_3 : S.HasOrthogonalProjection
rw rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 =
    HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (β := E) ((S.starProjection : (a : E) → E) x : E) ((Sᗮ.starProjection : (a : E) → E) x : E)‖ 2

Tactic:
rw [starProjection_add_starProjection_orthogonal]

Premises used: Submodule.starProjection_add_starProjection_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst_3 : S.HasOrthogonalProjection
simp :
  ‖HAdd.hAdd (α := E) (β := E) ((S.starProjection : (a : E) → E) x : E) ((Sᗮ.starProjection : (a : E) → E) x : E)‖ *
      ‖HAdd.hAdd (α := E) (β := E) ((S.starProjection : (a : E) → E) x : E) ((Sᗮ.starProjection : (a : E) → E) x : E)‖ =
    norm (E := ↥S) ((S.orthogonalProjection : (a : E) → ↥S) x : ↥S) *
        norm (E := ↥S) ((S.orthogonalProjection : (a : E) → ↥S) x : ↥S) +
      norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : E) → ↥Sᗮ) x : ↥Sᗮ) *
        norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : E) → ↥Sᗮ) x : ↥Sᗮ)
⊢ HPow.hPow (β := ℕ)
      ‖HAdd.hAdd (α := E) (β := E) ((S.starProjection : (a : E) → E) x : E) ((Sᗮ.starProjection : (a : E) → E) x : E)‖
      2 =
    HPow.hPow (β := ℕ) (norm (E := ↥S) ((S.orthogonalProjection : (a : E) → ↥S) x : ↥S)) 2 +
      HPow.hPow (β := ℕ) (norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : E) → ↥Sᗮ) x : ↥Sᗮ)) 2

Tactic:
simp only [sq]

Premises used: sq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst_3 : S.HasOrthogonalProjection
⊢ ‖HAdd.hAdd (α := E) (β := E) ((S.starProjection : (a : E) → E) x : E) ((Sᗮ.starProjection : (a : E) → E) x : E)‖ *
      ‖HAdd.hAdd (α := E) (β := E) ((S.starProjection : (a : E) → E) x : E) ((Sᗮ.starProjection : (a : E) → E) x : E)‖ =
    norm (E := ↥S) ((S.orthogonalProjection : (a : E) → ↥S) x : ↥S) *
        norm (E := ↥S) ((S.orthogonalProjection : (a : E) → ↥S) x : ↥S) +
      norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : E) → ↥Sᗮ) x : ↥Sᗮ) *
        norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : E) → ↥Sᗮ) x : ↥Sᗮ)

Tactic:
norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ <|
        (S.mem_orthogonal _).1 (Sᗮ.orthogonalProjection x).2 _ (S.orthogonalProjection x).2

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, setOf, Submodule.orthogonalProjection, Submodule.orthogonal, Submodule.mem_orthogonal, Iff.mp, Classical.choose, DFunLike.coe, Subtype.property, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst_3 : S.HasOrthogonalProjection
⊢ ‖HAdd.hAdd (α := E) (β := E) ((S.starProjection : (a : E) → E) x : E) ((Sᗮ.starProjection : (a : E) → E) x : E)‖ *
      ‖HAdd.hAdd (α := E) (β := E) ((S.starProjection : (a : E) → E) x : E) ((Sᗮ.starProjection : (a : E) → E) x : E)‖ =
    norm (E := ↥S) ((S.orthogonalProjection : (a : E) → ↥S) x : ↥S) *
        norm (E := ↥S) ((S.orthogonalProjection : (a : E) → ↥S) x : ↥S) +
      norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : E) → ↥Sᗮ) x : ↥Sᗮ) *
        norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : E) → ↥Sᗮ) x : ↥Sᗮ)

Tactic:
exact norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero _ _ <|
        (S.mem_orthogonal _).1 (Sᗮ.orthogonalProjection x).2 _ (S.orthogonalProjection x).2

Premises used: Submodule.orthogonalProjection, Submodule.orthogonal, Submodule.mem_orthogonal, Iff.mp, DFunLike.coe, Subtype.property, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Submodule 𝕜 E
inst_3 : S.HasOrthogonalProjection
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 =
    HPow.hPow (β := ℕ) (norm (E := E) ((S.starProjection : (a : E) → E) x : E)) 2 +
      HPow.hPow (β := ℕ) (norm (E := E) ((Sᗮ.starProjection : (a : E) → E) x : E)) 2

Tactic:
norm_sq_eq_add_norm_sq_projection x S

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, setOf, Submodule.norm_sq_eq_add_norm_sq_projection, Classical.choose
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
v : E
⊢ v ∈ U ↔ norm (E := E) ((U.starProjection : (a : E) → E) v : E) = ‖v‖

Tactic:
⟨fun h => norm_starProjection_apply _ h, fun h => ?_⟩

Premises used: Iff.intro, Submodule.norm_starProjection_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
v : E
refine : ∀ (h : norm (E := E) ((U.starProjection : (a : E) → E) v : E) = ‖v‖), v ∈ U
⊢ v ∈ U ↔ norm (E := E) ((U.starProjection : (a : E) → E) v : E) = ‖v‖

Tactic:
refine ⟨fun h => norm_starProjection_apply _ h, fun h => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
v : E
h : norm (E := E) ((U.starProjection : (a : E) → E) v : E) = ‖v‖
⊢ v ∈ U

Tactic:
simpa [h, sub_eq_zero, eq_comm (a := v), starProjection_eq_self_iff] using
    U.norm_sq_eq_add_norm_sq_starProjection v

Premises used: sub_eq_zero, Submodule.norm_sq_eq_add_norm_sq_starProjection, eq_comm, Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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 :
  ∀ (w : E),
    Eq (α := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) w : E)
      ((K.starProjection + Kᗮ.starProjection : (a : E) → E) w : E)
⊢ ContinuousLinearMap.id 𝕜 E = K.starProjection + Kᗮ.starProjection

Tactic:
ext w
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
w : E
⊢ Eq (α := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) w : E)
    ((K.starProjection + Kᗮ.starProjection : (a : E) → E) w : E)

Tactic:
(K.starProjection_add_starProjection_orthogonal w).symm

Premises used: Submodule.starProjection_add_starProjection_orthogonal, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
w : E
⊢ Eq (α := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) w : E)
    ((K.starProjection + Kᗮ.starProjection : (a : E) → E) w : E)

Tactic:
exact (K.starProjection_add_starProjection_orthogonal w).symm

Premises used: Submodule.starProjection_add_starProjection_orthogonal, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
u : ↥K
v : E
rw : ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ = ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ + 0
rw₁ rw₂ : ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ = ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫
⊢ ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ =
    ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ +
      ⟪HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E), (↑u : E)⟫

Tactic:
rw [starProjection_inner_eq_zero _ _ (Submodule.coe_mem _), add_zero]

Premises used: Submodule.starProjection_inner_eq_zero, Submodule.coe_mem, add_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
u : ↥K
v : E
rw :
  ⟪HAdd.hAdd (α := E) ((K.starProjection : (a : E) → E) v : E)
        (HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E)),
      (↑u : E)⟫ =
    ⟪v, (↑u : E)⟫
rw₁ rw₂ : ⟪v, (↑u : E)⟫ = ⟪v, (↑u : E)⟫
⊢ ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ +
      ⟪HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E), (↑u : E)⟫ =
    ⟪v, (↑u : E)⟫

Tactic:
rw [← inner_add_left, add_sub_cancel]

Premises used: inner_add_left, add_sub_cancel
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
u : ↥K
v : E
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(K.orthogonalProjection : (a : E) → ↥K) v, u⟫ = ⟪(↑u : E), v⟫
rw₁ :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(K.orthogonalProjection : (a : E) → ↥K) v, u⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, (↑u : E)⟫ : 𝕜)
rw₂ rw₃ :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, (↑u : E)⟫ : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, (↑u : E)⟫ : 𝕜)
⊢ ⟪u, (K.orthogonalProjection : (a : E) → ↥K) v⟫ = ⟪(↑u : E), v⟫

Tactic:
rw [← inner_conj_symm, ← inner_conj_symm (u : E), inner_orthogonalProjection_eq_of_mem_right]

Premises used: Submodule.inner_orthogonalProjection_eq_of_mem_right, Subtype.val, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
u v : E
simp_rw :
  ⟪(↑((K.orthogonalProjection : (a : E) → ↥K) u) : E), v⟫ = ⟪u, (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)⟫
simp_rw₁ :
  inner 𝕜 (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) u : ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) =
    ⟪u, (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)⟫
⊢ ⟪(K.starProjection : (a : E) → E) u, v⟫ = ⟪u, (K.starProjection : (a : E) → E) v⟫

Tactic:
simp_rw [starProjection_apply, ← inner_orthogonalProjection_eq_of_mem_left,
    inner_orthogonalProjection_eq_of_mem_right]

Premises used: Submodule.starProjection_apply, Submodule.inner_orthogonalProjection_eq_of_mem_right, Submodule.inner_orthogonalProjection_eq_of_mem_left
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
⊢ LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑K.starProjection : E →ₗ[𝕜] E)

Tactic:
inner_starProjection_left_eq_right K

Premises used: Submodule.inner_starProjection_left_eq_right, LinearMap.IsSymmetric
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
⊢ LinearMap.IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑U.starProjection : E →ₗ[𝕜] E)

Tactic:
⟨U.isIdempotentElem_starProjection.toLinearMap, U.starProjection_isSymmetric⟩

Premises used: ContinuousLinearMap.IsIdempotentElem.toLinearMap, LinearMap.IsSymmetricProjection.mk, Submodule.isIdempotentElem_starProjection, Submodule.starProjection_isSymmetric
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
⊢ IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p ↔
    ∃ (x : p.range.HasOrthogonalProjection), p = (↑p.range.starProjection : E →ₗ[𝕜] E)

Tactic:
⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isSymmetricProjection_starProjection _⟩

Premises used: Eq.rec, LinearMap.range, LinearMap.IsSymmetricProjection, _private.0.LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range.match_1, Submodule.isSymmetricProjection_starProjection, Iff.intro, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
refine :
  ∀ (hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p),
    ∃ (x : p.range.HasOrthogonalProjection), p = (↑p.range.starProjection : E →ₗ[𝕜] E)
⊢ IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p ↔
    ∃ (x : p.range.HasOrthogonalProjection), p = (↑p.range.starProjection : E →ₗ[𝕜] E)

Tactic:
refine ⟨fun hp ↦ ?_, fun ⟨h, hp⟩ ↦ hp ▸ isSymmetricProjection_starProjection _⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
⊢ p.range.HasOrthogonalProjection

Tactic:
have : (LinearMap.range p).HasOrthogonalProjection := hp.hasOrthogonalProjection_range
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
⊢ ∃ (x : p.range.HasOrthogonalProjection), p = (↑p.range.starProjection : E →ₗ[𝕜] E)

Tactic:
⟨this, Eq.symm ?_⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
refine : (↑p.range.starProjection : E →ₗ[𝕜] E) = p
⊢ ∃ (x : p.range.HasOrthogonalProjection), p = (↑p.range.starProjection : E →ₗ[𝕜] E)

Tactic:
refine ⟨this, Eq.symm ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
h : ∀ (x : E), Eq (α := E) (((↑p.range.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) ((p : (a : E) → E) x : E)
⊢ (↑p.range.starProjection : E →ₗ[𝕜] E) = p

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
x : E
⊢ Membership.mem (α := E) p.range ((p : (a : E) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
x : E
h : HSub.hSub (β := E) x ((p : (a : E) → E) x : E) ∈ p.rangeᗮ
⊢ Eq (α := E) (((↑p.range.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) ((p : (a : E) → E) x : E)

Tactic:
refine Submodule.eq_starProjection_of_mem_orthogonal (by simp) ?_

Premises used: Submodule.eq_starProjection_of_mem_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
x : E
h : HSub.hSub (β := E) x ((p : (a : E) → E) x : E) ∈ p.ker
⊢ HSub.hSub (β := E) x ((p : (a : E) → E) x : E) ∈ p.rangeᗮ

Tactic:
rw [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric]

Premises used: LinearMap.IsSymmetricProjection.isIdempotentElem, LinearMap.IsSymmetricProjection.isSymmetric, LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
x : E
⊢ HSub.hSub (β := E) x ((p : (a : E) → E) x : E) ∈ p.ker

Tactic:
simpa using congr($hp.isIdempotentElem.mul_one_sub_self x)
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
w : Submodule 𝕜 E
w_1 : w.HasOrthogonalProjection
⊢ LinearMap.IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑w.starProjection : E →ₗ[𝕜] E)

Tactic:
isSymmetricProjection_starProjection _

Premises used: Submodule.isSymmetricProjection_starProjection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
w : Submodule 𝕜 E
w_1 : w.HasOrthogonalProjection
⊢ LinearMap.IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑w.starProjection : E →ₗ[𝕜] E)

Tactic:
exact isSymmetricProjection_starProjection _

Premises used: Submodule.isSymmetricProjection_starProjection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
⊢ Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E) ↔ v ∈ Kᗮ

Tactic:
⟨fun h w hw => ?_, fun hv => ?_⟩

Premises used: Iff.intro