awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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'
p : Submodule 𝕜 E
inst_5 : p.HasOrthogonalProjection
inst_6 : (map f.toLinearMap p).HasOrthogonalProjection
x : E
refine_1 :
  Membership.mem (α := E') (map f.toLinearMap p) ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E')
⊢ Eq.{u_5 + 1} (α := E') ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E')
    (((map f.toLinearMap p).starProjection : (a : E') → E') ((f : (a : E) → E') x : E') : E')
have refine_2 : ∀ (y : E') (hy : y ∈ map f.toLinearMap p),
  ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
        ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
      y⟫ =
    0
Tactic: refine (eq_starProjection_of_mem_of_inner_eq_zero ?_ fun y hy => ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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'
p : Submodule 𝕜 E
inst_5 : p.HasOrthogonalProjection
inst_6 : (map f.toLinearMap p).HasOrthogonalProjection
x : E
y : E'
hy : y ∈ map f.toLinearMap p
⊢ ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
        ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
      y⟫ =
    0
have refine_2 : ∀ (x' : E) (hx' : x' ∈ (↑p : Set E)),
  ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
        ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
      (f : (a : E) → E') x'⟫ =
    0
Tactic: rcases hy with ⟨x', hx', rfl : f x' = y⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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'
p : Submodule 𝕜 E
inst_5 : p.HasOrthogonalProjection
inst_6 : (map f.toLinearMap p).HasOrthogonalProjection
x x' : E
hx' : x' ∈ (↑p : Set E)
⊢ ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
        ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
      (f : (a : E) → E') x'⟫ =
    0
have refine_2 : inner.{u_1, u_5} 𝕜 (E := E') ((f : (a : E) → E') (HSub.hSub (β := E) x ((p.starProjection : (a : E) → E) x : E)) : E')
    ((f : (a : E) → E') x' : E') =
  0
Tactic: rw [← f.map_sub, f.inner_map_map, starProjection_inner_eq_zero x x' hx']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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'
p : Submodule 𝕜 E
inst_5 : p.HasOrthogonalProjection
inst_6 : (map f.toLinearMap p).HasOrthogonalProjection
x x' : E
hx' : x' ∈ (↑p : Set E)
refine_2 :
  inner.{u_1, u_5} 𝕜 (E := E') ((f : (a : E) → E') (HSub.hSub (β := E) x ((p.starProjection : (a : E) → E) x : E)) : E')
      ((f : (a : E) → E') x' : E') =
    0
⊢ ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
        ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
      (f : (a : E) → E') x'⟫ =
    0
have refine_2₁ : ⟪HSub.hSub (β := E) x ((p.starProjection : (a : E) → E) x : E), x'⟫ = 0
Tactic: rw [← f.map_sub, f.inner_map_map, starProjection_inner_eq_zero x x' hx']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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'
p : Submodule 𝕜 E
inst_5 : p.HasOrthogonalProjection
inst_6 : (map f.toLinearMap p).HasOrthogonalProjection
x x' : E
hx' : x' ∈ (↑p : Set E)
refine_2 :
  inner.{u_1, u_5} 𝕜 (E := E') ((f : (a : E) → E') (HSub.hSub (β := E) x ((p.starProjection : (a : E) → E) x : E)) : E')
      ((f : (a : E) → E') x' : E') =
    0
refine_2₁ : ⟪HSub.hSub (β := E) x ((p.starProjection : (a : E) → E) x : E), x'⟫ = 0
⊢ ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
        ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
      (f : (a : E) → E') x'⟫ =
    0
have refine_2₂ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [← f.map_sub, f.inner_map_map, starProjection_inner_eq_zero x x' hx']
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_2 + 1} (α := E →L[𝕜] E) (starProjection ⊥) 0
have rw : Eq.{u_2 + 1} (α := E →L[𝕜] E) (ContinuousLinearMap.comp (M₂ := ↥⊥) (subtypeL ⊥) (orthogonalProjection ⊥)) 0
Tactic: rw [starProjection, orthogonalProjection_bot, ContinuousLinearMap.comp_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
rw : Eq.{u_2 + 1} (α := E →L[𝕜] E) (ContinuousLinearMap.comp (M₂ := ↥⊥) (subtypeL ⊥) (orthogonalProjection ⊥)) 0
⊢ Eq.{u_2 + 1} (α := E →L[𝕜] E) (starProjection ⊥) 0
have rw₁ : Eq.{u_2 + 1} (α := E →L[𝕜] E) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := ↥⊥) (subtypeL ⊥) 0) 0
Tactic: rw [starProjection, orthogonalProjection_bot, ContinuousLinearMap.comp_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
rw : Eq.{u_2 + 1} (α := E →L[𝕜] E) (ContinuousLinearMap.comp (M₂ := ↥⊥) (subtypeL ⊥) (orthogonalProjection ⊥)) 0
rw₁ : Eq.{u_2 + 1} (α := E →L[𝕜] E) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := ↥⊥) (subtypeL ⊥) 0) 0
⊢ Eq.{u_2 + 1} (α := E →L[𝕜] E) (starProjection ⊥) 0
have rw₂ : Eq.{u_2 + 1} (α := E →L[𝕜] E) 0 0
Tactic: rw [starProjection, orthogonalProjection_bot, ContinuousLinearMap.comp_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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.orthogonalProjection‖ * ‖v‖ ≤ 1 * ‖v‖
have hbc : ‖K.orthogonalProjection‖ ≤ 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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 := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) ≤ ‖v‖
have K₁ : ‖K.orthogonalProjection‖ * ‖v‖ ≤ 1 * ‖v‖
Tactic: calc
  ‖orthogonalProjection K v‖ ≤ ‖orthogonalProjection K‖ * ‖v‖ := K.orthogonalProjection.le_opNorm _
  _ ≤ 1 * ‖v‖ := by gcongr; exact orthogonalProjection_norm_le K
  _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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‖
⊢ norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) ≤ ‖v‖
have K₂ : 1 * ‖v‖ = ‖v‖
Tactic: calc
  ‖orthogonalProjection K v‖ ≤ ‖orthogonalProjection K‖ * ‖v‖ := K.orthogonalProjection.le_opNorm _
  _ ≤ 1 * ‖v‖ := by gcongr; exact orthogonalProjection_norm_le K
  _ = _ := by simp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
have refine : 1 ≤ ‖K.orthogonalProjection‖
Tactic: refine le_antisymm K.orthogonalProjection_norm_le ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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 ≠ ⊥
⊢ 1 ≤ ‖K.orthogonalProjection‖
have obtain : ∀ (x : E) (hxK : x ∈ K) (hx_ne_zero : x ≠ 0), 1 ≤ ‖K.orthogonalProjection‖
Tactic: obtain ⟨x, hxK, hx_ne_zero⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hK
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := E) (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)
      ((starProjection (𝕜 ∙ v) : (a : E) → E) w : E) =
    ⟪v, w⟫ • v
have suffices : (starProjection (𝕜 ∙ v) : (a : E) → E) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w) = ⟪v, w⟫ • v
Tactic: suffices ((𝕜 ∙ v).starProjection (((‖v‖ : 𝕜) ^ 2) • w)) = ⟪v, w⟫ • v by
    simpa using this
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w) = ⟪v, w⟫ • v
have hvm : Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ v) (⟪v, w⟫ • v)
Tactic: apply eq_starProjection_of_mem_of_inner_eq_zero
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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)
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w) = ⟪v, w⟫ • v
have hvo : ∀ (w_1 : E),
  Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ v) w_1 → ⟪HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0
Tactic: apply eq_starProjection_of_mem_of_inner_eq_zero
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ v) (⟪v, w⟫ • v)
have hvm : ∃ (a : 𝕜), a • v = ⟪v, w⟫ • v
Tactic: rw [Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ ∃ (a : 𝕜), a • v = ⟪v, w⟫ • v
have w₁ : 𝕜
Tactic: use ⟪v, w⟫
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
w₁ : 𝕜
⊢ ∃ (a : 𝕜), a • v = ⟪v, w⟫ • v
have h : ⟪v, w⟫ • v = ⟪v, w⟫ • v
Tactic: use ⟪v, w⟫
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ ∀ (w_1 : E),
    Membership.mem (γ := Submodule 𝕜 E) (𝕜 ∙ v) w_1 →
      ⟪HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w - ⟪v, w⟫ • v, w_1⟫ = 0
have hvo : ⟪HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 • w - ⟪v, w⟫ • v, v⟫ = 0
Tactic: rw [← Submodule.mem_orthogonal', Submodule.mem_orthogonal_singleton_iff_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
v w : E
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
have pos : ∀ (hv : v = 0), (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
have neg : ∀ (hv : ¬v = 0), (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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 (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
have pos : (starProjection (𝕜 ∙ 0) : (a : E) → E) w =
  HSMul.hSMul (β := E) (⟪0, w⟫ / (↑(HPow.hPow (β := ℕ) (norm.{u_2} (E := E) 0) 2) : 𝕜)) 0
Tactic: rw [hv]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (hypothesis)
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 (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
have hv' : ‖v‖ ≠ 0
Tactic: have hv' : ‖v‖ ≠ 0 := ne_of_gt (norm_pos_iff.mpr hv)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (hypothesis)
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
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
have 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)
Tactic: convert! key using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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)
⊢ (starProjection (𝕜 ∙ v) : (a : E) → E) w = (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v
have h₁ : (⟪v, w⟫ / (↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)) • v = ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
Tactic: convert! key using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
⊢ (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)
have match_scalars : 1 = (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)⁻¹ * HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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) : 𝕜)) • v = ((↑(HPow.hPow (β := ℕ) ‖v‖ 2) : 𝕜)⁻¹ * ⟪v, w⟫) • v
have match_scalars : ⟪v, w⟫ / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2 * 1 = (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖v‖ : 𝕜) 2)⁻¹ * ⟪v, w⟫ * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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 = ⟪v, w⟫ • v
have 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)
Tactic: rw [← smul_starProjection_singleton 𝕜 w]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
⊢ ⟪v, u⟫ = 0
have h₁ : v = HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E)
Tactic: convert! starProjection_inner_eq_zero v u hu using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (hypothesis)
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
⊢ v = HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E)
have this : Eq (α := ↥U) ((U.orthogonalProjection : (a : E) → ↥U) v : ↥U) (0 : ↥U)
Tactic: have : U.orthogonalProjection v = 0 := DFunLike.congr_fun h (⟨_, hv⟩ : V)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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)
⊢ v = HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E)
have h₁ : v = v - (↑((U.orthogonalProjection : (a : E) → ↥U) v) : E)
Tactic: rw [starProjection_apply, this, Submodule.coe_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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)
⊢ v = HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E)
have h₂ : v = v - (↑0 : E)
Tactic: rw [starProjection_apply, this, Submodule.coe_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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)
⊢ v = HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E)
have h₃ : v = v - 0
Tactic: rw [starProjection_apply, this, Submodule.coe_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
⊢ v = HSub.hSub (β := E) v ((U.starProjection : (a : E) → E) v : E)
have h₄ : v = v
Tactic: rw [starProjection_apply, this, Submodule.coe_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
have refine : ∀ (h : U.starProjection ∘SL V.starProjection = 0), U ⟂ V
Tactic: refine ⟨fun h => ?_, fun h => h.starProjection_comp_starProjection⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
⊢ U ⟂ V
have rw : U.orthogonalProjection ∘SL V.subtypeL = 0
Tactic: rw [← orthogonalProjection_comp_subtypeL_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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
⊢ U.orthogonalProjection ∘SL V.subtypeL = 0
have 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)
Tactic: simp only [ContinuousLinearMap.ext_iff, ContinuousLinearMap.comp_apply, subtypeL_apply,
    starProjection_apply, ContinuousLinearMap.zero_apply, coe_eq_zero] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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 (α := E) ((Kᗮ.starProjection : (a : E) → E) v : E) (0 : E)
have rw : Eq (α := ↥Kᗮ) ((Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) v : ↥Kᗮ) (0 : ↥Kᗮ)
Tactic: rw [starProjection_apply, coe_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
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.starProjection ∘SL V.starProjection : (a : E) → E) x : E) ((U.starProjection : (a : E) → E) x : E)
have nth_rw : Eq (α := E) (((U.subtypeL ∘SL U.orthogonalProjection) ∘SL V.starProjection : (a : E) → E) x : E)
  ((U.starProjection : (a : E) → E) x : E)
Tactic: nth_rw 1 [starProjection]