awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
rw :
  HPow.hPow (β := ℕ)
        (norm.{u_4} (E := ↥K)
          (WithLp.fst (p := 2) (β := ↥Kᗮ)
            (((K.prodEquivOfIsCompl Kᗮ ⋯).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ᗮ ⋯).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
⊢ 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‖

Tactic:
rw [← sq_eq_sq₀ (by positivity) (by positivity), WithLp.prod_norm_sq_eq_of_L2,
      K.norm_sq_eq_add_norm_sq_projection]

Premises used: Submodule.norm_sq_eq_add_norm_sq_projection, WithLp.prod_norm_sq_eq_of_L2, sq_eq_sq₀
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
⊢ HPow.hPow (β := ℕ)
        (norm.{u_4} (E := ↥K)
          (WithLp.fst (p := 2) (β := ↥Kᗮ)
            (((K.prodEquivOfIsCompl Kᗮ ⋯).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ᗮ ⋯).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:
simp [starProjection_apply_eq_isComplProjection]

Premises used: Submodule.starProjection_apply_eq_isComplProjection
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
x : E
⊢ Eq (α := WithLp 2 (↥K × ↥Kᗮ)) ((K.orthogonalDecomposition : (a : E) → WithLp 2 (↥K × ↥Kᗮ)) x : WithLp 2 (↥K × ↥Kᗮ))
    (WithLp.toLp 2 ((K.orthogonalProjection : (a : E) → ↥K) x, (Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) x) :
      WithLp 2 (↥K × ↥Kᗮ))

Tactic:
simp [orthogonalDecomposition, orthogonalProjection_apply_eq_linearProjOfIsCompl]

Premises used: Submodule.orthogonalDecomposition, Submodule.orthogonalProjection_apply_eq_linearProjOfIsCompl
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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.toLinearEquiv =
    (K.prodEquivOfIsCompl Kᗮ ⋯).symm ≪≫ₗ LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ))

Tactic:
rfl

Premises used: LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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.symm.toLinearEquiv = WithLp.linearEquiv 2 𝕜 (↥K × ↥Kᗮ) ≪≫ₗ K.prodEquivOfIsCompl Kᗮ ⋯

Tactic:
rfl

Premises used: LinearEquiv.symm, Set.Mem, LinearEquiv.trans, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
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ᗮ))
⊢ (↑(↑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

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
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:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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.symm : WithLp 2 (↥K × ↥Kᗮ) ≃L[𝕜] E) : WithLp 2 (↥K × ↥Kᗮ) →L[𝕜] E) =
    ContinuousLinearMap.coprod K.subtypeL Kᗮ.subtypeL ∘SL
      (↑(WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ) : WithLp 2 (↥K × ↥Kᗮ) →L[𝕜] ↥K × ↥Kᗮ)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
x : E
⊢ Eq (α := ↥K) (WithLp.fst (p := 2) (β := ↥Kᗮ) ((K.orthogonalDecomposition : (a : E) → WithLp 2 (↥K × ↥Kᗮ)) x) : ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K) x : ↥K)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
x : E
⊢ Eq (α := ↥Kᗮ) (WithLp.snd (p := 2) (α := ↥K) ((K.orthogonalDecomposition : (a : E) → WithLp 2 (↥K × ↥Kᗮ)) x) : ↥Kᗮ)
    ((Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) x : ↥Kᗮ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
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)
⊢ WithLp.fstL 2 𝕜 ↥K ↥Kᗮ ∘SL
      (↑(↑K.orthogonalDecomposition : E ≃L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) : E →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) =
    K.orthogonalProjection

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
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:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
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)
⊢ WithLp.sndL 2 𝕜 ↥K ↥Kᗮ ∘SL
      (↑(↑K.orthogonalDecomposition : E ≃L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) : E →L[𝕜] WithLp 2 (↥K × ↥Kᗮ)) =
    Kᗮ.orthogonalProjection

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.ProdL2
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
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:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
rcases :
  ∀ (w : E) (hwK : w ∈ K) (hw : ‖v - w‖ = ⨅ (w : (↑(↑K : Set E) : Type u_2)), ‖v - (↑w : E)‖), ∃ w ∈ K, v - w ∈ Kᗮ
⊢ ∃ 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⟩

Premises used: Iff.mp, completeSpace_coe_iff_isComplete, Submodule.exists_norm_eq_iInf_of_complete_subspace
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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ᗮ

Tactic:
⟨w, hwK, (K.mem_orthogonal' _).2 ?_⟩

Premises used: Iff.mpr, Submodule.mem_orthogonal', And.intro, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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)‖
refine : ∀ u ∈ K, ⟪v - w, u⟫ = 0
⊢ ∃ w ∈ K, v - w ∈ Kᗮ

Tactic:
refine ⟨w, hwK, (K.mem_orthogonal' _).2 ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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)‖
rwa rwa₁ rwa₂ rwa₃ : ‖v - w‖ = ⨅ (w : ↥K), ‖v - (↑w : E)‖
⊢ ∀ u ∈ K, ⟪v - w, u⟫ = 0

Tactic:
rwa [← K.norm_eq_iInf_iff_inner_eq_zero hwK]

Premises used: Submodule.norm_eq_iInf_iff_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
rcases : ∀ (w : E) (hwK : w ∈ K) (hw : v - w ∈ Kᗮ), ∃ w ∈ Kᗮ, v - w ∈ Kᗮᗮ
⊢ ∃ w ∈ Kᗮ, v - w ∈ Kᗮᗮ

Tactic:
rcases HasOrthogonalProjection.exists_orthogonal (K := K) v with ⟨w, hwK, hw⟩

Premises used: Submodule.HasOrthogonalProjection.exists_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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ᗮᗮ

Tactic:
⟨_, hw, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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ᗮ
refine : v - (v - w) ∈ Kᗮᗮ
⊢ ∃ w ∈ Kᗮ, v - w ∈ Kᗮᗮ

Tactic:
refine ⟨_, hw, ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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ᗮ
rw : w ∈ Kᗮᗮ
⊢ v - (v - w) ∈ Kᗮᗮ

Tactic:
rw [sub_sub_cancel]

Premises used: sub_sub_cancel
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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ᗮᗮ

Tactic:
K.le_orthogonal_orthogonal hwK

Premises used: Submodule.le_orthogonal_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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ᗮᗮ

Tactic:
exact K.le_orthogonal_orthogonal hwK

Premises used: Submodule.le_orthogonal_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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'
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)ᗮ
⊢ ∃ 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⟩

Premises used: LinearIsometryEquiv.symm, Submodule.HasOrthogonalProjection.exists_orthogonal, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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)ᗮ

Tactic:
⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Submodule.mem_map_of_mem, DFunLike.coe, Set.forall_mem_image
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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ᗮ
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
⊢ ∃ w ∈ map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K, v - w ∈ (map (↑f.toLinearEquiv : E →ₗ[𝕜] E') K)ᗮ

Tactic:
refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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ᗮ
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:
simp [← f.symm.inner_map_map, hw u hu]

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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'
⊢ HasOrthogonalProjection
    (map
      (↑f.toLinearIsometry :
        [inst_8 : FunLike (E →ₗᵢ[𝕜] E') E E'] → [SemilinearMapClass (E →ₗᵢ[𝕜] E') (RingHom.id 𝕜) E E'] → E →ₗ[𝕜] E')
      K)

Tactic:
HasOrthogonalProjection.map_linearIsometryEquiv K f

Premises used: SemilinearMapClass.semilinearMap, Submodule.HasOrthogonalProjection.map_linearIsometryEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
v : E
⊢ Membership.mem (γ := Submodule 𝕜 E) ⊤ᗮ (v - v)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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_1 : Submodule 𝕜 E
K : ClosedSubmodule 𝕜 E
inst_5 : CompleteSpace E
this : IsClosed (↑K : Submodule 𝕜 E).carrier := ⋯
⊢ (↑K : Submodule 𝕜 E).HasOrthogonalProjection

Tactic:
infer_instance
-- 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.orthogonalProjectionFn v ∈ K

Tactic:
(HasOrthogonalProjection.exists_orthogonal (K := K) v).choose_spec.left

Premises used: Submodule.orthogonalProjectionFn, Exists.choose_spec, Set.Mem, And.left, Submodule.HasOrthogonalProjection.exists_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ ∀ w ∈ K, ⟪v - K.orthogonalProjectionFn v, w⟫ = 0

Tactic:
(K.mem_orthogonal' _).1 (HasOrthogonalProjection.exists_orthogonal (K := K) v).choose_spec.right

Premises used: Exists.choose_spec, Submodule.mem_orthogonal', And.right, Submodule.HasOrthogonalProjection.exists_orthogonal, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
rw : ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0
⊢ K.orthogonalProjectionFn u = v

Tactic:
rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜]

Premises used: sub_eq_zero, inner_self_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
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
⊢ K.orthogonalProjectionFn u - v ∈ K

Tactic:
have hvs : K.orthogonalProjectionFn u - v ∈ K :=
    Submodule.sub_mem K (orthogonalProjectionFn_mem u) hvm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
hvs : K.orthogonalProjectionFn u - v ∈ K
⊢ ⟪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
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
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
⊢ ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0

Tactic:
have huv : ⟪u - v, K.orthogonalProjectionFn u - v⟫ = 0 := hvo _ hvs
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
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
rw₃ rw₄ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0

Tactic:
rw [inner_sub_left, huo, huv, sub_zero]

Premises used: sub_zero, inner_sub_left
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
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

Tactic:
have houv : ⟪u - v - (u - K.orthogonalProjectionFn u), K.orthogonalProjectionFn u - v⟫ = 0 := by
    rw [inner_sub_left, huo, huv, sub_zero]