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
K₁ : ‖K.orthogonalProjection‖ * ‖v‖ ≤ 1 * ‖v‖
K₂ : 1 * ‖v‖ = ‖v‖
⊢ norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) ≤ ‖v‖

Tactic:
calc
  ‖orthogonalProjection K v‖ ≤ ‖orthogonalProjection K‖ * ‖v‖ := K.orthogonalProjection.le_opNorm _
  _ ≤ 1 * ‖v‖ := by gcongr; exact orthogonalProjection_norm_le K
  _ = _ := by simp

Premises used: ContinuousLinearMap.le_opNorm, Submodule.orthogonalProjection, DFunLike.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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ norm (E := E) ((K.starProjection : (a : E) → E) v : E) ≤ ‖v‖

Tactic:
K.norm_orthogonalProjection_apply_le v

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Submodule.norm_orthogonalProjection_apply_le, 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ LipschitzWith (α := E) (β := ↥K) 1 (⇑K.orthogonalProjection : (a : E) → ↥K)

Tactic:
ContinuousLinearMap.lipschitzWith_of_opNorm_le (orthogonalProjection_norm_le K)

Premises used: Set.Mem, ContinuousLinearMap.lipschitzWith_of_opNorm_le, Submodule.orthogonalProjection_norm_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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ LipschitzWith (α := E) (β := E) 1 (⇑K.starProjection : (a : E) → E)

Tactic:
ContinuousLinearMap.lipschitzWith_of_opNorm_le (starProjection_norm_le K)

Premises used: Submodule.starProjection_norm_le, ContinuousLinearMap.lipschitzWith_of_opNorm_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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
hK : K ≠ ⊥
⊢ ‖K.orthogonalProjection‖ = 1

Tactic:
le_antisymm K.orthogonalProjection_norm_le ?_

Premises used: le_antisymm, Submodule.orthogonalProjection_norm_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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
hK : K ≠ ⊥
refine : 1 ≤ ‖K.orthogonalProjection‖
⊢ ‖K.orthogonalProjection‖ = 1

Tactic:
refine le_antisymm K.orthogonalProjection_norm_le ?_

Premises used: le_antisymm, Submodule.orthogonalProjection_norm_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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
hK : K ≠ ⊥
obtain : ∀ (x : E) (hxK : x ∈ K) (hx_ne_zero : x ≠ 0), 1 ≤ ‖K.orthogonalProjection‖
⊢ 1 ≤ ‖K.orthogonalProjection‖

Tactic:
obtain ⟨x, hxK, hx_ne_zero⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hK

Premises used: Submodule.exists_mem_ne_zero_of_ne_bot
-- 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
hK : K ≠ ⊥
x : E
hxK : x ∈ K
hx_ne_zero : x ≠ 0
⊢ 1 ≤ ‖K.orthogonalProjection‖

Tactic:
simpa [K.norm_orthogonalProjection_apply hxK, norm_eq_zero, hx_ne_zero]
    using K.orthogonalProjection.ratio_le_opNorm x

Premises used: norm_eq_zero, ContinuousLinearMap.ratio_le_opNorm, Submodule.orthogonalProjection, Submodule.norm_orthogonalProjection_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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
hK : K ≠ ⊥
⊢ ‖K.starProjection‖ = 1

Tactic:
K.norm_orthogonalProjection hK

Premises used: ContinuousLinearMap.comp, Submodule.orthogonalProjectionFn, Submodule.starProjection, Set.Mem, setOf, ContinuousLinearMap.opNorm, Submodule.orthogonalProjection, Classical.choose, Submodule.norm_orthogonalProjection
-- 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 w : E
this : (starProjection (𝕜 ∙ v) : (a : E) → E) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w) = ⟪v, w⟫ • v
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ⟪v, w⟫ • v

Tactic:
simpa using this
-- 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 w : E
suffices : (starProjection (𝕜 ∙ v) : (a : E) → E) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w) = ⟪v, w⟫ • v
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ⟪v, w⟫ • v

Tactic:
suffices ((𝕜 ∙ v).starProjection (((‖v‖ : 𝕜) ^ 2) • w)) = ⟪v, w⟫ • v by
    simpa using this
-- 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 w : E
hvm : Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ v) (⟪v, w⟫ • v)
hvo :
  ∀ (w_1 : E),
    Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ v) w_1 →
      ⟪HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w) = ⟪v, w⟫ • v

Tactic:
apply eq_starProjection_of_mem_of_inner_eq_zero

Premises used: Submodule.eq_starProjection_of_mem_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
v w : E
hvm : ∃ (a : 𝕜), a • v = ⟪v, w⟫ • v
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ v) (⟪v, w⟫ • v)

Tactic:
rw [Submodule.mem_span_singleton]

Premises used: Submodule.mem_span_singleton
-- 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 w : E
w₁ : 𝕜
h : ⟪v, w⟫ • v = ⟪v, w⟫ • v
⊢ ∃ (a : 𝕜), a • v = ⟪v, w⟫ • v

Tactic:
use ⟪v, 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
v w : E
hvo : ⟪HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w - ⟪v, w⟫ • v, v⟫ = 0
⊢ ∀ (w_1 : E),
    Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ v) w_1 →
      ⟪HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0

Tactic:
rw [← Submodule.mem_orthogonal', Submodule.mem_orthogonal_singleton_iff_inner_left]

Premises used: Submodule.mem_orthogonal', Submodule.mem_orthogonal_singleton_iff_inner_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
v w : E
⊢ ⟪HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w - ⟪v, w⟫ • v, v⟫ = 0

Tactic:
simp [inner_sub_left, inner_smul_left, inner_self_eq_norm_sq_to_K, mul_comm]

Premises used: inner_self_eq_norm_sq_to_K, inner_sub_left, mul_comm, inner_smul_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
v w : E
pos : ∀ (hv : v = 0), (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
neg : ∀ (hv : ¬v = 0), (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v

Tactic:
by_cases hv : v = 0
-- 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 w : E
hv : v = 0
pos :
  (starProjection (𝕜 ∙ 0) : (a : E) → E) w =
    HSMul.hSMul (β := E) (⟪0, w⟫ / (↑(HPow.hPow (β := ℕ) (norm.{u_2} (E := E) 0) 2) : 𝕜)) 0
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v

Tactic:
rw [hv]
-- 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 w : E
hv : v = 0
⊢ (starProjection (𝕜 ∙ 0) : (a : E) → E) w =
    HSMul.hSMul (β := E) (⟪0, w⟫ / (↑(HPow.hPow (β := ℕ) (norm.{u_2} (E := E) 0) 2) : 𝕜)) 0

Tactic:
simp [Submodule.span_zero_singleton 𝕜]

Premises used: Submodule.span_zero_singleton
-- 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 w : E
hv : ¬v = 0
⊢ ‖v‖ ≠ 0

Tactic:
have hv' : ‖v‖ ≠ 0 := ne_of_gt (norm_pos_iff.mpr hv)
-- 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 w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
⊢ HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v

Tactic:
simp [mul_smul, smul_starProjection_singleton 𝕜 w, -map_pow]

Premises used: Submodule.smul_starProjection_singleton, map_pow, SemigroupAction.mul_smul
-- 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 w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
⊢ HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v

Tactic:
have key :
    (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ((‖v‖ ^ 2 : ℝ) : 𝕜)) • (𝕜 ∙ v).starProjection w =
      (((‖v‖ ^ 2 : ℝ) : 𝕜)⁻¹ * ⟪v, w⟫) • v := by
    simp [mul_smul, smul_starProjection_singleton 𝕜 w, -map_pow]
-- 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 w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
⊢ HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v

Tactic:
key
-- 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 w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
h :
  (starProjection (𝕜 ∙ v) : (a : E) → E) w =
    HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E)
h₁ : (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v = ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v

Tactic:
convert! key using 1
-- 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 w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
match_scalars : 1 = (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 * 1
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w =
    HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E)

Tactic:
match_scalars
-- 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 w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
match_scalars :
  ⟪v, w⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 * 1 = (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)⁻¹ * ⟪v, w⟫ * 1
⊢ (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v = ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v

Tactic:
match_scalars
-- 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 w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
⊢ 1 = (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 * 1

Tactic:
field_simp [hv']
-- 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 w : E
hv : ¬v = 0
hv' : ‖v‖ ≠ 0
key :
  HSMul.hSMul (β := E) (HMul.hMul (α := 𝕜) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜))
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
⊢ ⟪v, w⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 * 1 = (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)⁻¹ * ⟪v, w⟫ * 1

Tactic:
field_simp [hv']
-- 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
hv : ‖v‖ = 1
w : E
rw :
  (starProjection (𝕜 ∙ v) : (a : E) → E) w =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E)
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = ⟪v, w⟫ • v

Tactic:
rw [← smul_starProjection_singleton 𝕜 w]

Premises used: Submodule.smul_starProjection_singleton
-- 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
hv : ‖v‖ = 1
w : E
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w =
    HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E)

Tactic:
simp [hv]
-- 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
⊢ v = (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) + (v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : 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
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_eq_zero_iff.mpr hv

Premises used: Iff.mpr, Submodule.orthogonalProjection_eq_zero_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
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
h : U ⟂ V
⊢ U.orthogonalProjection ∘SL V.subtypeL = 0

Tactic:
ContinuousLinearMap.ext fun v =>
    orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero <| h.symm v.prop

Premises used: Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.IsOrtho.symm, Subtype.prop, ContinuousLinearMap.ext
-- 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
⊢ U.starProjection ∘SL V.starProjection =
    U.subtypeL ∘SL (U.orthogonalProjection ∘SL V.subtypeL) ∘SL V.orthogonalProjection

Tactic:
simp only [starProjection, ContinuousLinearMap.comp_assoc]

Premises used: Submodule.starProjection, ContinuousLinearMap.comp_assoc
-- 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
⊢ U.subtypeL ∘SL (U.orthogonalProjection ∘SL V.subtypeL) ∘SL V.orthogonalProjection = 0

Tactic:
simp [h.orthogonalProjection_comp_subtypeL]

Premises used: Submodule.IsOrtho.orthogonalProjection_comp_subtypeL
-- 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
h : U.orthogonalProjection ∘SL V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ ⟪HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E), u⟫ = 0

Tactic:
starProjection_inner_eq_zero v u hu

Premises used: Submodule.starProjection_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
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
h : U.orthogonalProjection ∘SL V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
h₁ : v = HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E)
⊢ ⟪v, u⟫ = 0

Tactic:
convert! starProjection_inner_eq_zero v u hu using 2

Premises used: Submodule.starProjection_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
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
h : U.orthogonalProjection ∘SL V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
⊢ Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) v : ↥U) (0 : ↥U)

Tactic:
have : U.orthogonalProjection v = 0 := DFunLike.congr_fun h (⟨_, hv⟩ : V)
-- 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
h : U.orthogonalProjection ∘SL V.subtypeL = 0
u : E
hu : u ∈ U
v : E
hv : v ∈ V
this : Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) v : ↥U) (0 : ↥U)
h₁ : v = v - (↑((U.orthogonalProjection : (a : E) → ↥U) v) : E)
h₂ : v = v - (↑0 : E)
h₃ : v = v - 0
h₄ h₅ : v = v
⊢ v = HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E)

Tactic:
rw [starProjection_apply, this, Submodule.coe_zero, sub_zero]

Premises used: sub_zero, Submodule.starProjection_apply, Submodule.coe_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
⊢ U.starProjection ∘SL V.starProjection = 0 ↔ U ⟂ V

Tactic:
⟨fun h => ?_, fun h => h.starProjection_comp_starProjection⟩

Premises used: Submodule.IsOrtho.starProjection_comp_starProjection, Iff.intro
-- 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
refine : ∀ (h : U.starProjection ∘SL V.starProjection = 0), U ⟂ V
⊢ U.starProjection ∘SL V.starProjection = 0 ↔ U ⟂ V

Tactic:
refine ⟨fun h => ?_, fun h => h.starProjection_comp_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.starProjection ∘SL V.starProjection = 0
rw : U.orthogonalProjection ∘SL V.subtypeL = 0
⊢ U ⟂ V

Tactic:
rw [← orthogonalProjection_comp_subtypeL_eq_zero_iff]

Premises used: Submodule.orthogonalProjection_comp_subtypeL_eq_zero_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
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
h : U.starProjection ∘SL V.starProjection = 0
simp :
  ∀
    (h :
      ∀ (x : E),
        Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) (↑((V.orthogonalProjection : (a : E) → ↥V) x) : E)) 0)
    (x : ↥V), Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) (↑x : E) : ↥U) (0 : ↥U)
⊢ U.orthogonalProjection ∘SL V.subtypeL = 0

Tactic:
simp only [ContinuousLinearMap.ext_iff, ContinuousLinearMap.comp_apply, subtypeL_apply,
    starProjection_apply, ContinuousLinearMap.zero_apply, coe_eq_zero] at h ⊢

Premises used: Submodule.starProjection_apply, ContinuousLinearMap.ext_iff, Submodule.subtypeL_apply, Submodule.coe_eq_zero, ContinuousLinearMap.zero_apply, ContinuousLinearMap.comp_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 V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
h :
  ∀ (x : E), Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) (↑((V.orthogonalProjection : (a : E) → ↥V) x) : E)) 0
x : ↥V
⊢ Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) (↑x : E) : ↥U) (0 : ↥U)

Tactic:
simpa using h (x : E)

Premises used: Subtype.val
-- 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_mem_subspace_orthogonalComplement_eq_zero (K.le_orthogonal_orthogonal hv)

Premises used: Submodule.le_orthogonal_orthogonal, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_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
rw : Eq (α := ↥Kᗮ) ((Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) v : ↥Kᗮ) (0 : ↥Kᗮ)
⊢ Eq (α := E) ((Kᗮ.starProjection : (a : E) → E) v : E) (0 : E)

Tactic:
rw [starProjection_apply, coe_eq_zero]

Premises used: Submodule.starProjection_apply, Submodule.coe_eq_zero