awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
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
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (houv : ⟪K.orthogonalProjectionFn u - v, K.orthogonalProjectionFn u - v⟫ = 0),
    ⟪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

Premises used: sub_sub_sub_cancel_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
v : E
set :
  let p := K.orthogonalProjectionFn v;
  ‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖
⊢ ‖v‖ * ‖v‖ =
    ‖v - K.orthogonalProjectionFn v‖ * ‖v - K.orthogonalProjectionFn v‖ +
      ‖K.orthogonalProjectionFn v‖ * ‖K.orthogonalProjectionFn v‖

Tactic:
set p := K.orthogonalProjectionFn v

Premises used: Submodule.orthogonalProjectionFn
-- 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
p : E := K.orthogonalProjectionFn v
⊢ ⟪v - p, p⟫ = 0

Tactic:
have h' : ⟪v - p, p⟫ = 0 :=
    orthogonalProjectionFn_inner_eq_zero _ _ (orthogonalProjectionFn_mem v)
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
p : E := K.orthogonalProjectionFn v
h' : ⟪v - p, p⟫ = 0
⊢ ‖v - p + p‖ * ‖v - p + p‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖

Tactic:
norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (v - p) p h'

Premises used: HSub.hSub, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
p : E := K.orthogonalProjectionFn v
h' : ⟪v - p, p⟫ = 0
h h₁ : ‖v‖ = ‖v - p + p‖
⊢ ‖v‖ * ‖v‖ = ‖v - p‖ * ‖v - p‖ + ‖p‖ * ‖p‖

Tactic:
convert! norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (v - p) p h' using 2

Premises used: HSub.hSub, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
p : E := K.orthogonalProjectionFn v
h' : ⟪v - p, p⟫ = 0
⊢ ‖v‖ = ‖v - p + p‖

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 : K.HasOrthogonalProjection
x y : E
⊢ 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)
-- 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
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
rw₃ : HAdd.hAdd (α := 𝕜) 0 0 = 0
rw₄ rw₅ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪x + y - (K.orthogonalProjectionFn x + 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]

Premises used: Submodule.orthogonalProjectionFn_inner_eq_zero, inner_add_left, add_sub_add_comm, add_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
x y : E
hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
⊢ ∀ w ∈ K, ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0

Tactic:
have ho :
          ∀ w ∈ K, ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0 := by
          intro w hw
          rw [add_sub_add_comm, inner_add_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            orthogonalProjectionFn_inner_eq_zero _ w hw, add_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
x y : E
hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
ho : ∀ w ∈ K, ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0
a :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn (x + y)) ⋯) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) ⋯ +
          Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn 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) ⋯

Tactic:
ext
-- 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
x y : E
hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
ho : ∀ w ∈ K, ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0
⊢ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn (x + y)) ⋯) : E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) ⋯ +
          Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn y) ⋯) :
      E)

Tactic:
simp [eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hm ho]

Premises used: Submodule.eq_orthogonalProjectionFn_of_mem_of_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
c : 𝕜
x : E
⊢ c • K.orthogonalProjectionFn x ∈ K

Tactic:
have hm : c • K.orthogonalProjectionFn x ∈ K :=
          Submodule.smul_mem K _ (orthogonalProjectionFn_mem x)
-- 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
c : 𝕜
x : E
hm : c • K.orthogonalProjectionFn x ∈ K
w : E
hw : w ∈ K
rw : ⟪c • (x - K.orthogonalProjectionFn x), w⟫ = 0
rw₁ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) ⟪x - K.orthogonalProjectionFn x, w⟫ = 0
rw₂ : HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (0 : 𝕜) = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0

Tactic:
rw [← smul_sub, inner_smul_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            mul_zero]

Premises used: Submodule.orthogonalProjectionFn_inner_eq_zero, MulZeroClass.mul_zero, smul_sub, inner_smul_left
-- 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
c : 𝕜
x : E
hm : c • K.orthogonalProjectionFn x ∈ K
⊢ ∀ w ∈ K, ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0

Tactic:
have ho : ∀ w ∈ K, ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0 := by
          intro w hw
          rw [← smul_sub, inner_smul_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            mul_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
c : 𝕜
x : E
hm : c • K.orthogonalProjectionFn x ∈ K
ho : ∀ w ∈ K, ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0
a :
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn (c • x)) ⋯) : E) =
    (↑(HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) ⋯)) :
      E)
⊢ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn (c • x)) ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) ⋯)

Tactic:
ext
-- 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
c : 𝕜
x : E
hm : c • K.orthogonalProjectionFn x ∈ K
ho : ∀ w ∈ K, ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0
⊢ (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn (c • x)) ⋯) : E) =
    (↑(HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
          (Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) ⋯)) :
      E)

Tactic:
simp [eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hm ho]

Premises used: Submodule.eq_orthogonalProjectionFn_of_mem_of_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
x : E
simp :
  norm (E := ↥K)
      (({ toFun := fun (v : E) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn v) ⋯, map_add' := ⋯ :
              E →ₙ+ ↥K } :
            (a : E) → ↥K)
          x :
        ↥K) ≤
    ‖x‖
⊢ norm (E := ↥K)
      (({ toFun := fun (v : E) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn v) ⋯, map_add' := ⋯,
              map_smul' := ⋯ : E →ₗ[𝕜] ↥K } :
            (a : E) → ↥K)
          x :
        ↥K) ≤
    1 * ‖x‖

Tactic:
simp only [one_mul, LinearMap.coe_mk]

Premises used: LinearMap.coe_mk, one_mul
-- 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
x : E
⊢ norm (E := ↥K)
      (({ toFun := fun (v : E) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn v) ⋯, map_add' := ⋯ :
              E →ₙ+ ↥K } :
            (a : E) → ↥K)
          x :
        ↥K) ≤
    ‖x‖

Tactic:
le_of_pow_le_pow_left₀ two_ne_zero (norm_nonneg _) ?_

Premises used: two_ne_zero, le_of_pow_le_pow_left₀, norm_nonneg
-- 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
x : E
refine :
  HPow.hPow (β := ℕ)
      (norm (E := ↥K)
        (({ toFun := fun (v : E) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn v) ⋯, map_add' := ⋯ :
                E →ₙ+ ↥K } :
              (a : E) → ↥K)
            x :
          ↥K))
      2 ≤
    HPow.hPow (β := ℕ) ‖x‖ 2
⊢ norm (E := ↥K)
      (({ toFun := fun (v : E) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn v) ⋯, map_add' := ⋯ :
              E →ₙ+ ↥K } :
            (a : E) → ↥K)
          x :
        ↥K) ≤
    ‖x‖

Tactic:
refine le_of_pow_le_pow_left₀ two_ne_zero (norm_nonneg _) ?_

Premises used: two_ne_zero, le_of_pow_le_pow_left₀, norm_nonneg
-- 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
x : E
change : HPow.hPow (β := ℕ) ‖K.orthogonalProjectionFn x‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ HPow.hPow (β := ℕ)
      (norm (E := ↥K)
        (({ toFun := fun (v : E) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn v) ⋯, map_add' := ⋯ :
                E →ₙ+ ↥K } :
              (a : E) → ↥K)
            x :
          ↥K))
      2 ≤
    HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
change ‖K.orthogonalProjectionFn x‖ ^ 2 ≤ ‖x‖ ^ 2

Premises used: Submodule.orthogonalProjectionFn
-- 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
x : E
nlinarith :
  HPow.hPow (β := ℕ) ‖x‖ 2 < HPow.hPow (β := ℕ) ‖K.orthogonalProjectionFn x‖ 2 →
    0 - ‖x - K.orthogonalProjectionFn x‖ * ‖x - K.orthogonalProjectionFn x‖ +
          (HPow.hPow (β := ℕ) ‖x‖ 2 - HPow.hPow (β := ℕ) ‖K.orthogonalProjectionFn x‖ 2) +
        -(‖x‖ * ‖x‖ -
            (‖x - K.orthogonalProjectionFn x‖ * ‖x - K.orthogonalProjectionFn x‖ +
              ‖K.orthogonalProjectionFn x‖ * ‖K.orthogonalProjectionFn x‖)) =
      0
⊢ HPow.hPow (β := ℕ) ‖K.orthogonalProjectionFn x‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
nlinarith [K.orthogonalProjectionFn_norm_sq x]

Premises used: Submodule.orthogonalProjectionFn_norm_sq
-- 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.orthogonalProjection : (a : E) → ↥K) v) : E)

Tactic:
rfl

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Classical.choose, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
v : E
⊢ Eq (α := E) ((U.starProjection : (a : E) → E) v : E) ((↑((U.orthogonalProjection : (a : E) → ↥U) v) : E) : E)

Tactic:
rfl

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Classical.choose, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
v : E
⊢ Eq (α := E) ((↑((U.orthogonalProjection : (a : E) → ↥U) v) : E) : E) ((U.starProjection : (a : E) → E) v : E)

Tactic:
rfl

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Classical.choose, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
x : E
⊢ Membership.mem (α := E) U ((U.starProjection : (a : E) → E) x : E)

Tactic:
simp only [starProjection_apply, SetLike.coe_mem]

Premises used: SetLike.coe_mem, Submodule.starProjection_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ ∀ w ∈ K, ⟪HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E), w⟫ = 0

Tactic:
orthogonalProjectionFn_inner_eq_zero v

Premises used: Submodule.orthogonalProjectionFn, Submodule.orthogonalProjectionFn_inner_eq_zero, Set.Mem, Classical.choose
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v w : E
hw : w ∈ K
rw : ⟪HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E), w⟫ = 0
⊢ ⟪w, HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E)⟫ = 0

Tactic:
rw [inner_eq_zero_symm]

Premises used: inner_eq_zero_symm
-- 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 w : E
hw : w ∈ K
⊢ ⟪HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E), w⟫ = 0

Tactic:
starProjection_inner_eq_zero _ _ hw

Premises used: Submodule.starProjection_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v w : E
hw : w ∈ K
⊢ ⟪HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E), w⟫ = 0

Tactic:
exact starProjection_inner_eq_zero _ _ hw

Premises used: Submodule.starProjection_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hvm : v ∈ K
hvo : ∀ w ∈ K, ⟪u - v, w⟫ = 0
⊢ (K.starProjection : (a : E) → E) u = v

Tactic:
eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hvm hvo

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Classical.choose, Submodule.eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v : E
hv : v ∈ K
hvo : u - v ∈ Kᗮ
⊢ (K.starProjection : (a : E) → E) u = v

Tactic:
eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero hv <| (Submodule.mem_orthogonal' _ _).1 hvo

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Submodule.mem_orthogonal', Iff.mp, Classical.choose, Submodule.eq_orthogonalProjectionFn_of_mem_of_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
u v z : E
hv : v ∈ K
hz : z ∈ Kᗮ
hu : u = v + z
⊢ u - v ∈ Kᗮ

Tactic:
simpa [hu]
-- 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 : E
⊢ (Kᗮ.starProjection : (a : E) → E) u = HSub.hSub (β := E) u ((K.starProjection : (a : E) → E) u : E)

Tactic:
eq_starProjection_of_mem_orthogonal' (sub_starProjection_mem_orthogonal _)
    (K.le_orthogonal_orthogonal (K.orthogonalProjection u).2) <| (sub_add_cancel _ _).symm

Premises used: Submodule.le_orthogonal_orthogonal, Submodule.sub_starProjection_mem_orthogonal, Submodule.orthogonalProjection, Submodule.eq_starProjection_of_mem_orthogonal', Eq.symm, sub_add_cancel, DFunLike.coe, Subtype.property
-- 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 : E
⊢ (Kᗮ.orthogonalProjection : (a : E) → ↥Kᗮ) u =
    Subtype.mk (p := fun (x : E) ↦ x ∈ Kᗮ) (HSub.hSub (β := E) u ((K.starProjection : (a : E) → E) u : E)) ⋯

Tactic:
Subtype.ext <| starProjection_orthogonal_val _

Premises used: Submodule.starProjection_orthogonal_val, Subtype.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
h :
  ∀ (x : E),
    Eq (α := E) ((Uᗮ.starProjection : (a : E) → E) x : E)
      ((ContinuousLinearMap.id 𝕜 E - U.starProjection : (a : E) → E) x : E)
⊢ Uᗮ.starProjection = ContinuousLinearMap.id 𝕜 E - U.starProjection

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
x : E
h :
  Eq (α := E)
    ((Uᗮ.subtypeL : (a : ↥Uᗮ) → E)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ Uᗮ)
          (HSub.hSub (β := E) x ((U.subtypeL : (a : ↥U) → E) ((U.orthogonalProjection : (a : E) → ↥U) x : ↥U) : E)) ⋯) :
      E)
    ((ContinuousLinearMap.id 𝕜 E - U.subtypeL ∘SL U.orthogonalProjection : (a : E) → E) x : E)
⊢ Eq (α := E) ((Uᗮ.starProjection : (a : E) → E) x : E)
    ((ContinuousLinearMap.id 𝕜 E - U.starProjection : (a : E) → E) x : E)

Tactic:
simp only [starProjection, ContinuousLinearMap.comp_apply,
    orthogonalProjection_orthogonal]

Premises used: Submodule.starProjection, Submodule.orthogonalProjection_orthogonal, ContinuousLinearMap.comp_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
x : E
⊢ Eq (α := E)
    ((Uᗮ.subtypeL : (a : ↥Uᗮ) → E)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ Uᗮ)
          (HSub.hSub (β := E) x ((U.subtypeL : (a : ↥U) → E) ((U.orthogonalProjection : (a : E) → ↥U) x : ↥U) : E)) ⋯) :
      E)
    ((ContinuousLinearMap.id 𝕜 E - U.subtypeL ∘SL U.orthogonalProjection : (a : E) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
⊢ Uᗮ.starProjection = 1 - U.starProjection

Tactic:
starProjection_orthogonal U

Premises used: Submodule.starProjection_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
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
y : E
rw : ∀ w ∈ U, ⟪y - (↑((U.orthogonalProjection : (a : E) → ↥U) y) : E), w⟫ = 0
⊢ ‖HSub.hSub (β := E) y ((U.starProjection : (a : E) → E) y : E)‖ = ⨅ (x : ↥U), ‖y - (↑x : E)‖

Tactic:
rw [starProjection_apply, U.norm_eq_iInf_iff_inner_eq_zero (Submodule.coe_mem _)]

Premises used: Submodule.norm_eq_iInf_iff_inner_eq_zero, Submodule.starProjection_apply, Submodule.coe_mem