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
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
⊢ ⟪x + y - (K.orthogonalProjectionFn x + K.orthogonalProjectionFn y), w⟫ = 0
have rw₄ : Eq.{u_1 + 1} (α := 𝕜) 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]
-- 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
hm : K.orthogonalProjectionFn x + K.orthogonalProjectionFn y ∈ K
⊢ 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 ho : ∀ 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]
-- 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
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)) ⋯ =
    Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) ⋯ +
      Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn y) ⋯
have a : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn (x + y)) sorry) : E) =
  (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) sorry +
        Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn y) sorry) :
    E)
Tactic: ext
-- 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
c : 𝕜
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) ⋯)
have hm : c • K.orthogonalProjectionFn x ∈ K
Tactic: have hm : c • K.orthogonalProjectionFn x ∈ K :=
          Submodule.smul_mem K _ (orthogonalProjectionFn_mem x)
-- 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
c : 𝕜
x : E
hm : c • K.orthogonalProjectionFn x ∈ K
w : E
hw : w ∈ K
⊢ ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0
have rw : ⟪c • (x - K.orthogonalProjectionFn x), w⟫ = 0
Tactic: rw [← smul_sub, inner_smul_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            mul_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
c : 𝕜
x : E
hm : c • K.orthogonalProjectionFn x ∈ K
w : E
hw : w ∈ K
rw : ⟪c • (x - K.orthogonalProjectionFn x), w⟫ = 0
⊢ ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0
have rw₁ : HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) ⟪x - K.orthogonalProjectionFn x, w⟫ = 0
Tactic: rw [← smul_sub, inner_smul_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            mul_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
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
⊢ ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0
have rw₂ : HMul.hMul (α := 𝕜) (β := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜) (0 : 𝕜) = 0
Tactic: rw [← smul_sub, inner_smul_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            mul_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
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
⊢ ⟪c • x - c • K.orthogonalProjectionFn x, w⟫ = 0
have rw₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [← smul_sub, inner_smul_left, orthogonalProjectionFn_inner_eq_zero _ w hw,
            mul_zero]
-- 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
c : 𝕜
x : E
hm : c • K.orthogonalProjectionFn x ∈ K
⊢ 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) ⋯)
have ho : ∀ 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]
-- 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
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)) ⋯ =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) ⋯)
have a : (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn (c • x)) sorry) : E) =
  (↑(HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
        (Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn x) sorry)) :
    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 : K.HasOrthogonalProjection
x : E
⊢ 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‖
have simp : norm (E := ↥K)
    (({ toFun := fun (v : E) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn v) sorry, map_add' := sorry :
            E →ₙ+ ↥K } :
          (a : E) → ↥K)
        x :
      ↥K) ≤
  ‖x‖
Tactic: simp only [one_mul, LinearMap.coe_mk]
-- 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 : 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‖
have refine : HPow.hPow (β := ℕ)
    (norm (E := ↥K)
      (({ toFun := fun (v : E) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ K) (K.orthogonalProjectionFn v) sorry, map_add' := sorry :
              E →ₙ+ ↥K } :
            (a : E) → ↥K)
          x :
        ↥K))
    2 ≤
  HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: refine le_of_pow_le_pow_left₀ two_ne_zero (norm_nonneg _) ?_
-- 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 : E
⊢ 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
have change : HPow.hPow (β := ℕ) ‖K.orthogonalProjectionFn x‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: change ‖K.orthogonalProjectionFn x‖ ^ 2 ≤ ‖x‖ ^ 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 : K.HasOrthogonalProjection
x : E
⊢ HPow.hPow (β := ℕ) ‖K.orthogonalProjectionFn x‖ 2 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
have 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
Tactic: nlinarith [K.orthogonalProjectionFn_norm_sq 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v w : E
hw : w ∈ K
⊢ ⟪w, HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E)⟫ = 0
have rw : ⟪HSub.hSub (β := E) v ((K.starProjection : (a : E) → E) v : E), w⟫ = 0
Tactic: rw [inner_eq_zero_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
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
⊢ Uᗮ.starProjection = ContinuousLinearMap.id 𝕜 E - U.starProjection
have h : ∀ (x : E),
  Eq (α := E) ((Uᗮ.starProjection : (a : E) → E) x : E)
    ((ContinuousLinearMap.id 𝕜 E - U.starProjection : (a : E) → E) x : E)
Tactic: ext
-- 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
x : E
⊢ Eq (α := E) ((Uᗮ.starProjection : (a : E) → E) x : E)
    ((ContinuousLinearMap.id 𝕜 E - U.starProjection : (a : E) → E) x : E)
have 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)) sorry) :
    E)
  ((ContinuousLinearMap.id 𝕜 E - U.subtypeL ∘SL U.orthogonalProjection : (a : E) → E) x : E)
Tactic: simp only [starProjection, ContinuousLinearMap.comp_apply,
    orthogonalProjection_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
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
y : E
⊢ ‖HSub.hSub (β := E) y ((U.starProjection : (a : E) → E) y : E)‖ = ⨅ (x : ↥U), ‖y - (↑x : E)‖
have rw : ∀ w ∈ U, ⟪y - (↑((U.orthogonalProjection : (a : E) → ↥U) y) : E), w⟫ = 0
Tactic: rw [starProjection_apply, U.norm_eq_iInf_iff_inner_eq_zero (Submodule.coe_mem _)]
-- 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 : ↥K
⊢ (K.orthogonalProjection : (a : E) → ↥K) (↑v : E) = v
have a : (↑((K.orthogonalProjection : (a : E) → ↥K) (↑v : E)) : E) = (↑v : E)
Tactic: ext
-- 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 : ↥K
⊢ (↑((K.orthogonalProjection : (a : E) → ↥K) (↑v : E)) : E) = (↑v : E)
have a : (↑v : E) ∈ K
Tactic: apply eq_starProjection_of_mem_of_inner_eq_zero
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : ↥K
a : (↑v : E) ∈ K
⊢ (↑((K.orthogonalProjection : (a : E) → ↥K) (↑v : E)) : E) = (↑v : E)
have a₁ : ∀ w ∈ K, ⟪(↑v : E) - (↑v : E), w⟫ = 0
Tactic: apply eq_starProjection_of_mem_of_inner_eq_zero
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ (K.starProjection : (a : E) → E) v = v ↔ v ∈ K
have refine_1 : ∀ (h : (K.starProjection : (a : E) → E) v = v), v ∈ K
Tactic: refine ⟨fun h => ?_, fun h => eq_starProjection_of_mem_of_inner_eq_zero h ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
refine_1 : ∀ (h : (K.starProjection : (a : E) → E) v = v), v ∈ K
⊢ (K.starProjection : (a : E) → E) v = v ↔ v ∈ K
have refine_2 : ∀ (h : v ∈ K), ∀ w ∈ K, ⟪v - v, w⟫ = 0
Tactic: refine ⟨fun h => ?_, fun h => eq_starProjection_of_mem_of_inner_eq_zero h ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
h : (K.starProjection : (a : E) → E) v = v
⊢ v ∈ K
have refine_1 : Membership.mem (α := E) K ((K.starProjection : (a : E) → E) v : E)
Tactic: rw [← 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
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
⊢ (↑U.starProjection : E →ₗ[𝕜] E).range = U
have h : ∀ (x : E), x ∈ (↑U.starProjection : E →ₗ[𝕜] E).range ↔ x ∈ U
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
⊢ Eq (α := E →L[𝕜] E) (starProjection ⊤) (ContinuousLinearMap.id 𝕜 E)
have h : ∀ (x : E), Eq (α := E) ((starProjection ⊤ : (a : E) → E) x : E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E)
Tactic: ext
-- 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 (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K) ↔ v ∈ Kᗮ
have refine_1 : ∀ (h : Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K)), v ∈ Kᗮ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Subtype.ext <| eq_starProjection_of_mem_orthogonal
    (zero_mem _) ?_⟩
-- 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 (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K)), v ∈ Kᗮ
⊢ Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K) ↔ v ∈ Kᗮ
have refine_2 : ∀ (h : v ∈ Kᗮ), v - (↑0 : E) ∈ Kᗮ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Subtype.ext <| eq_starProjection_of_mem_orthogonal
    (zero_mem _) ?_⟩
-- 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 (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K)
⊢ v ∈ Kᗮ
have refine_1 : v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) ∈ Kᗮ
Tactic: rw [← sub_zero v, ← coe_zero (p := K), ← 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
⊢ (↑K.orthogonalProjection : E →ₗ[𝕜] ↥K).ker = Kᗮ
have h : ∀ (x : E), x ∈ (↑K.orthogonalProjection : E →ₗ[𝕜] ↥K).ker ↔ x ∈ Kᗮ
Tactic: ext
-- 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
⊢ (↑U.starProjection : E →ₗ[𝕜] E).ker = Uᗮ
have rw : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = Uᗮ
Tactic: rw [LinearMap.IsIdempotentElem.ker_eq_range U.isIdempotentElem_starProjection.toLinearMap,
    ← range_starProjection Uᗮ, starProjection_orthogonal, coe_sub, coe_id]
-- 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
rw : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = Uᗮ
⊢ (↑U.starProjection : E →ₗ[𝕜] E).ker = Uᗮ
have rw₁ : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = (↑Uᗮ.starProjection : E →ₗ[𝕜] E).range
Tactic: rw [LinearMap.IsIdempotentElem.ker_eq_range U.isIdempotentElem_starProjection.toLinearMap,
    ← range_starProjection Uᗮ, starProjection_orthogonal, coe_sub, coe_id]
-- 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
rw : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = Uᗮ
rw₁ : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = (↑Uᗮ.starProjection : E →ₗ[𝕜] E).range
⊢ (↑U.starProjection : E →ₗ[𝕜] E).ker = Uᗮ
have rw₂ : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range =
  (↑(ContinuousLinearMap.id 𝕜 E - U.starProjection) : E →ₗ[𝕜] E).range
Tactic: rw [LinearMap.IsIdempotentElem.ker_eq_range U.isIdempotentElem_starProjection.toLinearMap,
    ← range_starProjection Uᗮ, starProjection_orthogonal, coe_sub, coe_id]
-- 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
rw : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = Uᗮ
rw₁ : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = (↑Uᗮ.starProjection : E →ₗ[𝕜] E).range
rw₂ :
  (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range =
    (↑(ContinuousLinearMap.id 𝕜 E - U.starProjection) : E →ₗ[𝕜] E).range
⊢ (↑U.starProjection : E →ₗ[𝕜] E).ker = Uᗮ
have rw₃ : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range =
  ((↑(ContinuousLinearMap.id 𝕜 E) : E →ₗ[𝕜] E) - (↑U.starProjection : E →ₗ[𝕜] E)).range
Tactic: rw [LinearMap.IsIdempotentElem.ker_eq_range U.isIdempotentElem_starProjection.toLinearMap,
    ← range_starProjection Uᗮ, starProjection_orthogonal, coe_sub, coe_id]
-- 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
rw : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = Uᗮ
rw₁ : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = (↑Uᗮ.starProjection : E →ₗ[𝕜] E).range
rw₂ :
  (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range =
    (↑(ContinuousLinearMap.id 𝕜 E - U.starProjection) : E →ₗ[𝕜] E).range
rw₃ :
  (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range =
    ((↑(ContinuousLinearMap.id 𝕜 E) : E →ₗ[𝕜] E) - (↑U.starProjection : E →ₗ[𝕜] E)).range
⊢ (↑U.starProjection : E →ₗ[𝕜] E).ker = Uᗮ
have rw₄ : (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range
Tactic: rw [LinearMap.IsIdempotentElem.ker_eq_range U.isIdempotentElem_starProjection.toLinearMap,
    ← range_starProjection Uᗮ, starProjection_orthogonal, coe_sub, coe_id]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.Basic (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup E'
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst_5 : p.HasOrthogonalProjection
inst_6 : (map f.toLinearMap p).HasOrthogonalProjection
x : E
⊢ Eq.{u_5 + 1} (α := E') ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E')
    (((map f.toLinearMap p).starProjection : (a : E') → E') ((f : (a : E) → E') x : E') : E')
have refine_1 : Membership.mem (α := E') (map f.toLinearMap p) ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E')
Tactic: refine (eq_starProjection_of_mem_of_inner_eq_zero ?_ fun y hy => ?_).symm