awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ ∀ ⦃i j : ι₁ ⊕ ι₂⦄,
    i ≠ j →
      (fun (i j : ι₁ ⊕ ι₂) ↦
          inner 𝕜 (E := WithLp 2 (E × F))
              (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
                    (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
                  i :
                WithLp 2 (E × F))
              (((v.toBasis.prod w.toBasis).map (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (E × F))) :
                    (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F))
                  j :
                WithLp 2 (E × F)) =
            0)
        i j
have right : (∀ (a a_1 : ι₁), ¬a = a_1 → inner.{u_1, u_4} 𝕜 (E := E) ((v : (a : ι₁) → E) a : E) ((v : (a : ι₁) → E) a_1 : E) = 0) ∧
  ∀ (b b_1 : ι₂), ¬b = b_1 → inner.{u_1, u_5} 𝕜 (E := F) ((w : (a : ι₂) → F) b : F) ((w : (a : ι₂) → F) b_1 : F) = 0
Tactic: simp only [ne_eq, Basis.map_apply, Basis.prod_apply, LinearMap.coe_inl,
        OrthonormalBasis.coe_toBasis, LinearMap.coe_inr, WithLp.coe_symm_linearEquiv,
        WithLp.prod_inner_apply, Sum.forall, Sum.elim_inl, Function.comp_apply, inner_zero_right,
        add_zero, Sum.elim_inr, zero_add, Sum.inl.injEq, reduceCtorEq, not_false_eq_true,
        inner_zero_left, imp_self, implies_true, and_true, Sum.inr.injEq, true_and]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Fintype ι₁
inst_6 : Fintype ι₂
v : OrthonormalBasis ι₁ 𝕜 E
w : OrthonormalBasis ι₂ 𝕜 F
⊢ ∀ (i : ι₁ ⊕ ι₂),
    Eq (α := WithLp 2 (E × F)) ((v.prod w : (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F)) i : WithLp 2 (E × F))
      (Sum.elim (WithLp.toLp 2 ∘ Function.comp (β := E) (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) (⇑v : (a : ι₁) → E))
          (WithLp.toLp 2 ∘ Function.comp (β := F) (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) (⇑w : (a : ι₂) → F)) i :
        WithLp 2 (E × F))
have rw : (∀ (a : ι₁),
    Eq (α := WithLp 2 (E × F)) ((v.prod w : (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F)) (Sum.inl a) : WithLp 2 (E × F))
      (Sum.elim (β := ι₂)
          (WithLp.toLp 2 ∘ Function.comp (β := E) (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) (⇑v : (a : ι₁) → E))
          (WithLp.toLp 2 ∘ Function.comp (β := F) (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) (⇑w : (a : ι₂) → F))
          (Sum.inl a) :
        WithLp 2 (E × F))) ∧
  ∀ (b : ι₂),
    Eq (α := WithLp 2 (E × F)) ((v.prod w : (a : ι₁ ⊕ ι₂) → WithLp 2 (E × F)) (Sum.inr b) : WithLp 2 (E × F))
      (Sum.elim (α := ι₁)
          (WithLp.toLp 2 ∘ Function.comp (β := E) (⇑(LinearMap.inl 𝕜 E F) : (a : E) → E × F) (⇑v : (a : ι₁) → E))
          (WithLp.toLp 2 ∘ Function.comp (β := F) (⇑(LinearMap.inr 𝕜 E F) : (a : F) → E × F) (⇑w : (a : ι₂) → F))
          (Sum.inr b) :
        WithLp 2 (E × F))
Tactic: rw [Sum.forall]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x x_1 : E
⊢ norm (E := WithLp 2 (↥K × ↥Kᗮ))
      (((K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)) :
            (a : E) → WithLp 2 (↥K × ↥Kᗮ))
          x_1 :
        WithLp 2 (↥K × ↥Kᗮ)) =
    ‖x_1‖
have rw : HPow.hPow (β := ℕ)
      (norm.{u_4} (E := ↥K)
        (WithLp.fst (p := 2) (β := ↥Kᗮ)
          (((K.prodEquivOfIsCompl Kᗮ sorry).symm ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)) :
              (a : E) → WithLp 2 (↥K × ↥Kᗮ))
            x_1)))
      2 +
    HPow.hPow (β := ℕ)
      (norm.{u_4} (E := ↥Kᗮ)
        (WithLp.snd (p := 2) (α := ↥K)
          (((K.prodEquivOfIsCompl Kᗮ sorry).symm ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ)) :
              (a : E) → WithLp 2 (↥K × ↥Kᗮ))
            x_1)))
      2 =
  HPow.hPow (β := ℕ) (norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) x_1 : ↥K)) 2 +
    HPow.hPow (β := ℕ) (norm (E := ↥Kᗮ) ((Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) x_1 : ↥Kᗮ)) 2
Tactic: rw [← sq_eq_sq₀ (by positivity) (by positivity), WithLp.prod_norm_sq_eq_of_L2,
      K.norm_sq_eq_add_norm_sq_projection]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ (↑(↑K.orthogonalDecomposition : E ≃L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) : E →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) =
    (↑(ContinuousLinearEquiv.symm (WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ)) :
        ↥K × ↥Kᗮ →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) ∘SL
      K.orthogonalProjection.prod Kᗮ.orthogonalProjection
have h : ∀ (x : E),
  Eq (α := WithLp 2 (↥K × ↥Kᗮ))
    (((↑(↑K.orthogonalDecomposition : E ≃L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) : E →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) :
          (a : E) → WithLp 2 (↥K × ↥Kᗮ))
        x :
      WithLp 2 (↥K × ↥Kᗮ))
    (((↑(ContinuousLinearEquiv.symm (WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ)) :
              ↥K × ↥Kᗮ →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) ∘SL
            K.orthogonalProjection.prod Kᗮ.orthogonalProjection :
          (a : E) → WithLp 2 (↥K × ↥Kᗮ))
        x :
      WithLp 2 (↥K × ↥Kᗮ))
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ WithLp.fstL 2 𝕜 ↥K ↥Kᗮ ∘SL
      (↑(↑K.orthogonalDecomposition : E ≃L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) : E →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) =
    K.orthogonalProjection
have h : ∀ (x : E),
  Eq.{u_4 + 1} (α := E)
    (↑((WithLp.fstL 2 𝕜 ↥K ↥Kᗮ ∘SL
              (↑(↑K.orthogonalDecomposition : E ≃L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) : E →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) :
            (a : E) → ↥K)
          x) :
      E)
    (↑((K.orthogonalProjection : (a : E) → ↥K) x) : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.ProdL2 (goal)
Goal:
𝕜 : Type u_1
E : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ WithLp.sndL 2 𝕜 ↥K ↥Kᗮ ∘SL
      (↑(↑K.orthogonalDecomposition : E ≃L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) : E →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) =
    Kᗮ.orthogonalProjection
have h : ∀ (x : E),
  Eq.{u_4 + 1} (α := E)
    (↑((WithLp.sndL 2 𝕜 ↥K ↥Kᗮ ∘SL
              (↑(↑K.orthogonalDecomposition : E ≃L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) : E →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) :
            (a : E) → ↥Kᗮ)
          x) :
      E)
    (↑((Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) x) : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : CompleteSpace.{u_2} ↥K
v : E
⊢ ∃ w ∈ K, v - w ∈ Kᗮ
have rcases : ∀ (w : E) (hwK : w ∈ K) (hw : ‖v - w‖ = ⨅ (w : (↑(↑K : Set E) : Type u_2)), ‖v - (↑w : E)‖), ∃ w ∈ K, v - w ∈ Kᗮ
Tactic: rcases K.exists_norm_eq_iInf_of_complete_subspace (completeSpace_coe_iff_isComplete.mp ‹_›) v
      with ⟨w, hwK, hw⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : CompleteSpace.{u_2} ↥K
v w : E
hwK : w ∈ K
hw : ‖v - w‖ = ⨅ (w : (↑(↑K : Set E) : Type u_2)), ‖v - (↑w : E)‖
⊢ ∃ w ∈ K, v - w ∈ Kᗮ
have refine : ∀ u ∈ K, ⟪v - w, u⟫ = 0
Tactic: refine ⟨w, hwK, (K.mem_orthogonal' _).2 ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : CompleteSpace.{u_2} ↥K
v w : E
hwK : w ∈ K
hw : ‖v - w‖ = ⨅ (w : (↑(↑K : Set E) : Type u_2)), ‖v - (↑w : E)‖
⊢ ∀ u ∈ K, ⟪v - w, u⟫ = 0
have rwa : ‖v - w‖ = ⨅ (w : ↥K), ‖v - (↑w : E)‖
Tactic: rwa [← K.norm_eq_iInf_iff_inner_eq_zero hwK]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
v : E
⊢ ∃ w ∈ Kᗮ, v - w ∈ Kᗮᗮ
have rcases : ∀ (w : E) (hwK : w ∈ K) (hw : v - w ∈ Kᗮ), ∃ w ∈ Kᗮ, v - w ∈ Kᗮᗮ
Tactic: rcases HasOrthogonalProjection.exists_orthogonal (K := K) v with ⟨w, hwK, hw⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
v w : E
hwK : w ∈ K
hw : v - w ∈ Kᗮ
⊢ ∃ w ∈ Kᗮ, v - w ∈ Kᗮᗮ
have refine : v - (v - w) ∈ Kᗮᗮ
Tactic: refine ⟨_, hw, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
v w : E
hwK : w ∈ K
hw : v - w ∈ Kᗮ
⊢ v - (v - w) ∈ Kᗮᗮ
have rw : w ∈ Kᗮᗮ
Tactic: rw [sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
v : E'
⊢ ∃ w ∈ map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K, v - w ∈ (map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K)ᗮ
have rcases : ∀ (w : E) (hwK : w ∈ K) (hw : HSub.hSub (α := E) ((f.symm : (a : E') → E) v : E) w ∈ Kᗮ),
  ∃ w ∈ map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K, v - w ∈ (map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K)ᗮ
Tactic: rcases HasOrthogonalProjection.exists_orthogonal (K := K) (f.symm v) with ⟨w, hwK, hw⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
E' : Type u_4
inst_6 : NormedAddCommGroup E'
inst_7 : InnerProductSpace 𝕜 E'
f : E ≃ₗᵢ[𝕜] E'
v : E'
w : E
hwK : w ∈ K
hw : HSub.hSub (α := E) ((f.symm : (a : E') → E) v : E) w ∈ Kᗮ
⊢ ∃ w ∈ map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K, v - w ∈ (map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K)ᗮ
have refine : ∀ (u : E) (hu : u ∈ (↑K : Set E)),
  ⟪((↑f.toLinearEquiv : E →ₗ[𝕜] E') : (a : E) → E') u, HSub.hSub (β := E') v ((f : (a : E) → E') w : E')⟫ = 0
Tactic: refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩
-- 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
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
⊢ K.orthogonalProjectionFn u = v
have rw : ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0
Tactic: rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]
-- 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
⊢ ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0
have hvs : K.orthogonalProjectionFn u - v ∈ K
Tactic: have hvs : K.orthogonalProjectionFn u - v ∈ K :=
    Submodule.sub_mem K (orthogonalProjectionFn_mem u) hvm
-- 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
⊢ ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0
have huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
Tactic: have huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0 :=
    orthogonalProjectionFn_inner_eq_zero u _ hvs
-- 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
⊢ ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0
have huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0
Tactic: have huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0 := hvo _ hvs
-- 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
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0
⊢ ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0
have rw : ⟪u - v, K.orthogonalProjectionFn u - v⟫ - ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
Tactic: rw [inner_sub_left, huo, huv, 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0
rw : ⟪u - v, K.orthogonalProjectionFn u - v⟫ - ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
⊢ ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0
have rw₁ : ⟪u - v, K.orthogonalProjectionFn u - v⟫ - 0 = 0
Tactic: rw [inner_sub_left, huo, huv, 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0
rw : ⟪u - v, K.orthogonalProjectionFn u - v⟫ - ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
rw₁ : ⟪u - v, K.orthogonalProjectionFn u - v⟫ - 0 = 0
⊢ ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0
have rw₂ : HSub.hSub (α := 𝕜) 0 0 = 0
Tactic: rw [inner_sub_left, huo, huv, 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0
rw : ⟪u - v, K.orthogonalProjectionFn u - v⟫ - ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
rw₁ : ⟪u - v, K.orthogonalProjectionFn u - v⟫ - 0 = 0
rw₂ : HSub.hSub (α := 𝕜) 0 0 = 0
⊢ ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0
have rw₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [inner_sub_left, huo, huv, sub_zero]
-- 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0
⊢ ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0
have houv : ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0
Tactic: have houv : ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0 := by
    rw [inner_sub_left, huo, huv, 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
huo : ⟪u - K.orthogonalProjectionFn u, K.orthogonalProjectionFn u - v⟫ = 0
huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0
houv : ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0
⊢ ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0
have rwa : ∀ (houv : ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0),
  ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0
Tactic: rwa [sub_sub_sub_cancel_left] at houv
Cleared hypotheses: houv
-- 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
p : E := K.orthogonalProjectionFn v
⊢ ‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖
have h' : ⟪v - p, p⟫ = 0
Tactic: have h' : ⟪v - p, p⟫ = 0 :=
    orthogonalProjectionFn_inner_eq_zero _ _ (orthogonalProjectionFn_mem 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
p : E := K.orthogonalProjectionFn v
h' : ⟪v - p, p⟫ = 0
⊢ ‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖
have h : ‖v‖ = ‖v - p + p‖
Tactic: convert! norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (v - p) p h' using 2
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x y : E
⊢ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn (x + y)) ⋯ =
    Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) ⋯ +
      Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn y) ⋯
have hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
Tactic: have hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K :=
          Submodule.add_mem K (orthogonalProjectionFn_mem x) (orthogonalProjectionFn_mem y)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x y : E
hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
w : E
hw : w ∈ K
⊢ ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0
have rw : ⟪x - K.orthogonalProjectionFn x + (y - K.orthogonalProjectionFn y), w⟫ = 0
Tactic: rw [add_sub_add_comm, inner_add_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            orthogonalProjectionFn_inner_eq_zero _ w hw, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x y : E
hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
w : E
hw : w ∈ K
rw : ⟪x - K.orthogonalProjectionFn x + (y - K.orthogonalProjectionFn y), w⟫ = 0
⊢ ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0
have rw₁ : ⟪x - K.orthogonalProjectionFn x, w⟫ + ⟪y - K.orthogonalProjectionFn y, w⟫ = 0
Tactic: rw [add_sub_add_comm, inner_add_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            orthogonalProjectionFn_inner_eq_zero _ w hw, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x y : E
hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
w : E
hw : w ∈ K
rw : ⟪x - K.orthogonalProjectionFn x + (y - K.orthogonalProjectionFn y), w⟫ = 0
rw₁ : ⟪x - K.orthogonalProjectionFn x, w⟫ + ⟪y - K.orthogonalProjectionFn y, w⟫ = 0
⊢ ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0
have rw₂ : 0 + ⟪y - K.orthogonalProjectionFn y, w⟫ = 0
Tactic: rw [add_sub_add_comm, inner_add_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            orthogonalProjectionFn_inner_eq_zero _ w hw, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace ℝ F
K : Submodule 𝕜 E
inst_5 : K.HasOrthogonalProjection
x y : E
hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
w : E
hw : w ∈ K
rw : ⟪x - K.orthogonalProjectionFn x + (y - K.orthogonalProjectionFn y), w⟫ = 0
rw₁ : ⟪x - K.orthogonalProjectionFn x, w⟫ + ⟪y - K.orthogonalProjectionFn y, w⟫ = 0
rw₂ : 0 + ⟪y - K.orthogonalProjectionFn y, w⟫ = 0
⊢ ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0
have rw₃ : HAdd.hAdd (α := 𝕜) 0 0 = 0
Tactic: rw [add_sub_add_comm, inner_add_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            orthogonalProjectionFn_inner_eq_zero _ w hw, add_zero]