awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ Eq (α := E) ((starProjection (𝕜 ∙ v)ᗮ : (a : E) → E) v : E) (0 : E)
have rw : Eq (α := ↥(𝕜 ∙ v)ᗮ) ((orthogonalProjection (𝕜 ∙ v)ᗮ : (a : E) → ↥(𝕜 ∙ v)ᗮ) v : ↥(𝕜 ∙ v)ᗮ) (0 : ↥(𝕜 ∙ v)ᗮ)
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
x : E
S : Submodule 𝕜 E
inst_3 : S.HasOrthogonalProjection
⊢ 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
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [starProjection_add_starProjection_orthogonal]
-- 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
x : E
S : Submodule 𝕜 E
inst_3 : S.HasOrthogonalProjection
⊢ 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
have 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ᗮ)
Tactic: simp only [sq]
-- 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 : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
v : E
⊢ v ∈ U ↔ norm (E := E) ((U.starProjection : (a : E) → E) v : E) = ‖v‖
have refine : ∀ (h : norm (E := E) ((U.starProjection : (a : E) → E) v : E) = ‖v‖), v ∈ U
Tactic: refine ⟨fun h => norm_starProjection_apply _ h, fun 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
⊢ ContinuousLinearMap.id 𝕜 E = K.starProjection + Kᗮ.starProjection
have h : ∀ (w : E),
  Eq (α := E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) w : E)
    ((K.starProjection + Kᗮ.starProjection : (a : E) → E) w : E)
Tactic: ext 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u : ↥K
v : 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)⟫
have rw : ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ = ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ + 0
Tactic: rw [starProjection_inner_eq_zero _ _ (Submodule.coe_mem _), add_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
u : ↥K
v : E
rw : ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ = ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ + 0
⊢ ⟪(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)⟫
have rw₁ : ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ = ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫
Tactic: rw [starProjection_inner_eq_zero _ _ (Submodule.coe_mem _), add_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
u : ↥K
v : 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)⟫
have 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)⟫
Tactic: rw [← inner_add_left, add_sub_cancel]
-- 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
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)⟫
⊢ ⟪(K.starProjection : (a : E) → E) v, (↑u : E)⟫ +
      ⟪HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E), (↑u : E)⟫ =
    ⟪v, (↑u : E)⟫
have rw₁ : ⟪v, (↑u : E)⟫ = ⟪v, (↑u : E)⟫
Tactic: rw [← inner_add_left, add_sub_cancel]
-- 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
u : ↥K
v : E
⊢ ⟪u, (K.orthogonalProjection : (a : E) → ↥K) v⟫ = ⟪(↑u : E), v⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(K.orthogonalProjection : (a : E) → ↥K) v, u⟫ = ⟪(↑u : E), v⟫
Tactic: rw [← inner_conj_symm, ← inner_conj_symm (u : E), inner_orthogonalProjection_eq_of_mem_right]
-- 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
u : ↥K
v : E
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(K.orthogonalProjection : (a : E) → ↥K) v, u⟫ = ⟪(↑u : E), v⟫
⊢ ⟪u, (K.orthogonalProjection : (a : E) → ↥K) v⟫ = ⟪(↑u : E), v⟫
have rw₁ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(K.orthogonalProjection : (a : E) → ↥K) v, u⟫ : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, (↑u : E)⟫ : 𝕜)
Tactic: rw [← inner_conj_symm, ← inner_conj_symm (u : E), inner_orthogonalProjection_eq_of_mem_right]
-- 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
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)⟫ : 𝕜)
⊢ ⟪u, (K.orthogonalProjection : (a : E) → ↥K) v⟫ = ⟪(↑u : E), v⟫
have rw₂ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, (↑u : E)⟫ : 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, (↑u : E)⟫ : 𝕜)
Tactic: rw [← inner_conj_symm, ← inner_conj_symm (u : E), inner_orthogonalProjection_eq_of_mem_right]
-- 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
u v : E
⊢ ⟪(K.starProjection : (a : E) → E) u, v⟫ = ⟪u, (K.starProjection : (a : E) → E) v⟫
have simp_rw : ⟪(↑((K.orthogonalProjection : (a : E) → ↥K) u) : E), v⟫ = ⟪u, (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)⟫
Tactic: simp_rw [starProjection_apply, ← inner_orthogonalProjection_eq_of_mem_left,
    inner_orthogonalProjection_eq_of_mem_right]
-- 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
u v : E
simp_rw :
  ⟪(↑((K.orthogonalProjection : (a : E) → ↥K) u) : E), v⟫ = ⟪u, (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)⟫
⊢ ⟪(K.starProjection : (a : E) → E) u, v⟫ = ⟪u, (K.starProjection : (a : E) → E) v⟫
have 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)⟫
Tactic: simp_rw [starProjection_apply, ← inner_orthogonalProjection_eq_of_mem_left,
    inner_orthogonalProjection_eq_of_mem_right]
-- 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
p : E →ₗ[𝕜] E
⊢ IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p ↔
    ∃ (x : p.range.HasOrthogonalProjection), p = (↑p.range.starProjection : E →ₗ[𝕜] E)
have refine : ∀ (hp : 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 _⟩
-- 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
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
⊢ ∃ (x : p.range.HasOrthogonalProjection), p = (↑p.range.starProjection : E →ₗ[𝕜] E)
have this : p.range.HasOrthogonalProjection
Tactic: have : (LinearMap.range p).HasOrthogonalProjection := hp.hasOrthogonalProjection_range
-- 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
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)
have refine : (↑p.range.starProjection : E →ₗ[𝕜] E) = p
Tactic: refine ⟨this, Eq.symm ?_⟩
-- 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
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
⊢ (↑p.range.starProjection : E →ₗ[𝕜] E) = p
have h : ∀ (x : E), Eq (α := E) (((↑p.range.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) ((p : (a : E) → E) x : E)
Tactic: ext x
-- 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
p : E →ₗ[𝕜] E
hp : IsSymmetricProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) p
this : p.range.HasOrthogonalProjection
x : E
⊢ Eq (α := E) (((↑p.range.starProjection : E →ₗ[𝕜] E) : (a : E) → E) x : E) ((p : (a : E) → E) x : E)
have h : HSub.hSub (β := E) x ((p : (a : E) → E) x : E) ∈ p.rangeᗮ
Tactic: refine Submodule.eq_starProjection_of_mem_orthogonal (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
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.rangeᗮ
have h : HSub.hSub (β := E) x ((p : (a : E) → E) x : E) ∈ p.ker
Tactic: rw [hp.isIdempotentElem.isSymmetric_iff_orthogonal_range.mp hp.isSymmetric]
-- 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
⊢ Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E) ↔ v ∈ Kᗮ
have refine_1 : ∀ (h : Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)) (w : E) (hw : w ∈ K), ⟪w, v⟫ = 0
Tactic: refine ⟨fun h w hw => ?_, fun hv => ?_⟩
-- 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
refine_1 : ∀ (h : Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)) (w : E) (hw : w ∈ K), ⟪w, v⟫ = 0
⊢ Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E) ↔ v ∈ Kᗮ
have refine_2 : ∀ (hv : v ∈ Kᗮ), Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)
Tactic: refine ⟨fun h w hw => ?_, fun hv => ?_⟩
-- 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
h : Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)
w : E
hw : w ∈ K
⊢ ⟪w, v⟫ = 0
have refine_1 : ⟪(K.starProjection : (a : E) → E) w, v⟫ = 0
Tactic: rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h,
      inner_zero_right]
-- 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
h : Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)
w : E
hw : w ∈ K
refine_1 : ⟪(K.starProjection : (a : E) → E) w, v⟫ = 0
⊢ ⟪w, v⟫ = 0
have refine_1₁ : ⟪w, (K.starProjection : (a : E) → E) v⟫ = 0
Tactic: rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h,
      inner_zero_right]
-- 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
h : Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)
w : E
hw : w ∈ K
refine_1 : ⟪(K.starProjection : (a : E) → E) w, v⟫ = 0
refine_1₁ : ⟪w, (K.starProjection : (a : E) → E) v⟫ = 0
⊢ ⟪w, v⟫ = 0
have refine_1₂ : ⟪w, 0⟫ = 0
Tactic: rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h,
      inner_zero_right]
-- 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
h : Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)
w : E
hw : w ∈ K
refine_1 : ⟪(K.starProjection : (a : E) → E) w, v⟫ = 0
refine_1₁ : ⟪w, (K.starProjection : (a : E) → E) v⟫ = 0
refine_1₂ : ⟪w, 0⟫ = 0
⊢ ⟪w, v⟫ = 0
have refine_1₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h,
      inner_zero_right]
-- 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
⊢ (re : (a : 𝕜) → ℝ) ⟪(K.starProjection : (a : E) → E) v, v⟫ =
    HPow.hPow (β := ℕ) (norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K)) 2
have rw : ‖v‖ * ‖v‖ =
  ‖v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)‖ * ‖v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)‖ +
    norm.{u_2} (E := E) (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) *
      norm.{u_2} (E := E) (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)
Tactic: rw [starProjection_apply,
    re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
    div_eq_iff (NeZero.ne' 2).symm, pow_two, add_sub_assoc, ← eq_sub_iff_add_eq', coe_norm,
    ← mul_sub_one, show (2 : ℝ) - 1 = 1 by norm_num, mul_one, sub_eq_iff_eq_add', norm_sub_rev]
-- 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
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(K.starProjection : (a : E) → E) v, v⟫ : ℝ)
have rw : 0 ≤ HPow.hPow (β := ℕ) (norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K)) 2
Tactic: rw [re_inner_starProjection_eq_normSq K v]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have pos : ∀ (hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ),
  (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: by_cases hK : FiniteDimensional 𝕜 Kᗮ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
pos :
  ∀ (hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ),
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
      HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have neg : ∀ (hK : ¬FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ),
  (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: by_cases hK : FiniteDimensional 𝕜 Kᗮ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : ¬FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have neg : finrank 𝕜 E = 0
Tactic: rw [finrank_of_infinite_dimensional hK, pow_zero, LinearMap.det_eq_one_of_finrank_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
⊢ Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
have a : ∀ (val val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥K)),
  Eq.{u_1 + 1} (α := 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))
        (Sum.inl val) (Sum.inl val_1) :
      𝕜)
    (Matrix.fromBlocks (m := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (o := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 0 0 (-1)
        (Sum.inl val) (Sum.inl val_1) :
      𝕜)
Tactic: ext (_ | _) (_ | _)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
a :
  ∀ (val val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥K)),
    Eq.{u_1 + 1} (α := 𝕜)
      ((LinearMap.toMatrix b b :
            (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
              Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
          ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
            (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))
          (Sum.inl val) (Sum.inl val_1) :
        𝕜)
      (Matrix.fromBlocks (m := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (o := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 0 0 (-1)
          (Sum.inl val) (Sum.inl val_1) :
        𝕜)
⊢ Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
have a₁ : ∀ (val : Fin (finrank.{u_1, u_2} 𝕜 ↥K)) (val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)),
  Eq.{u_1 + 1} (α := 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))
        (Sum.inl val) (Sum.inr val_1) :
      𝕜)
    (Matrix.fromBlocks (l := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) (o := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 0 0 (-1)
        (Sum.inl val) (Sum.inr val_1) :
      𝕜)
Tactic: ext (_ | _) (_ | _)