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
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
y : E
⊢ ∀ w ∈ U, ⟪y - (↑((U.orthogonalProjection : (a : E) → ↥U) y) : E), w⟫ = 0

Tactic:
starProjection_inner_eq_zero _

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

Tactic:
exact starProjection_inner_eq_zero _

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 : ↥K
a : (↑((K.orthogonalProjection : (a : E) → ↥K) (↑v : E)) : E) = (↑v : E)
⊢ (K.orthogonalProjection : (a : E) → ↥K) (↑v : E) = v

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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : ↥K
a : (↑v : E) ∈ K
a₁ : ∀ w ∈ K, ⟪(↑v : E) - (↑v : E), w⟫ = 0
⊢ (↑((K.orthogonalProjection : (a : E) → ↥K) (↑v : E)) : E) = (↑v : E)

Tactic:
apply eq_starProjection_of_mem_of_inner_eq_zero

Premises used: Submodule.eq_starProjection_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
v : ↥K
⊢ (↑v : E) ∈ K

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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : ↥K
⊢ ∀ w ∈ K, ⟪(↑v : E) - (↑v : E), w⟫ = 0

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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : ↥K
⊢ (K.starProjection : (a : E) → E) (↑v : E) = (↑v : E)

Tactic:
simp [starProjection_apply]

Premises used: 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
⊢ (K.starProjection : (a : E) → E) v = v ↔ v ∈ K

Tactic:
⟨fun h => ?_, fun h => eq_starProjection_of_mem_of_inner_eq_zero h ?_⟩

Premises used: Submodule.eq_starProjection_of_mem_of_inner_eq_zero, Iff.intro
-- 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
refine_1 : ∀ (h : (K.starProjection : (a : E) → E) v = v), v ∈ K
refine_2 : ∀ (h : v ∈ K), ∀ w ∈ K, ⟪v - v, w⟫ = 0
⊢ (K.starProjection : (a : E) → E) v = v ↔ v ∈ K

Tactic:
refine ⟨fun h => ?_, fun h => eq_starProjection_of_mem_of_inner_eq_zero h ?_⟩
-- 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
h : (K.starProjection : (a : E) → E) v = v
refine_1 : Membership.mem (α := E) K ((K.starProjection : (a : E) → E) v : E)
⊢ v ∈ K

Tactic:
rw [← h]
-- 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
h : (K.starProjection : (a : E) → E) v = v
⊢ Membership.mem (α := E) K ((K.starProjection : (a : E) → E) v : 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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
h : v ∈ K
⊢ ∀ w ∈ K, ⟪v - v, w⟫ = 0

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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ Membership.mem (α := E) K (((↑K.starProjection : E →ₗ[𝕜] E) : (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
h : ∀ (x : E), x ∈ (↑U.starProjection : E →ₗ[𝕜] E).range ↔ x ∈ U
⊢ (↑U.starProjection : E →ₗ[𝕜] E).range = U

Tactic:
ext x
-- 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
⊢ x ∈ (↑U.starProjection : E →ₗ[𝕜] E).range ↔ x ∈ U

Tactic:
⟨fun ⟨y, hy⟩ ↦ hy ▸ coe_mem (U.orthogonalProjection y),
    fun h ↦ ⟨x, starProjection_eq_self_iff.mpr h⟩⟩

Premises used: Iff.mpr, Membership.mem, Eq.rec, Submodule.coe_mem, _private.0.Submodule.range_starProjection.match_1, Submodule.orthogonalProjection, Iff.intro, Exists.intro, DFunLike.coe, Submodule.starProjection_eq_self_iff
-- 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
⊢ x ∈ (↑U.starProjection : E →ₗ[𝕜] E).range ↔ x ∈ U

Tactic:
exact ⟨fun ⟨y, hy⟩ ↦ hy ▸ coe_mem (U.orthogonalProjection y),
    fun h ↦ ⟨x, starProjection_eq_self_iff.mpr h⟩⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
h : ∀ (x : E), Eq (α := E) ((starProjection ⊤ : (a : E) → E) x : E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E)
⊢ Eq (α := E →L[𝕜] E) (starProjection ⊤) (ContinuousLinearMap.id 𝕜 E)

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
x : E
⊢ Eq (α := E) ((starProjection ⊤ : (a : E) → E) x : E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E)

Tactic:
starProjection_eq_self_iff.mpr trivial

Premises used: Iff.mpr, trivial, Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Eq (α := E) ((starProjection ⊤ : (a : E) → E) x : E) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) x : E)

Tactic:
exact starProjection_eq_self_iff.mpr trivial
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_2 + 1} (α := E →L[𝕜] E) (starProjection ⊤) 1

Tactic:
starProjection_top

Premises used: Submodule.starProjection_top
-- 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
⊢ Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K) ↔ v ∈ Kᗮ

Tactic:
⟨fun h ↦ ?_, fun h ↦ Subtype.ext <| eq_starProjection_of_mem_orthogonal
    (zero_mem _) ?_⟩

Premises used: Submodule.eq_starProjection_of_mem_orthogonal, Iff.intro, ZeroMemClass.zero_mem, 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
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ᗮ
refine_2 : ∀ (h : v ∈ Kᗮ), v - (↑0 : E) ∈ Kᗮ
⊢ 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 _) ?_⟩
-- 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
h : Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K)
refine_1 : v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) ∈ Kᗮ
⊢ v ∈ Kᗮ

Tactic:
rw [← sub_zero v, ← coe_zero (p := K), ← h]

Premises used: sub_zero, Submodule.coe_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
h : Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K)
⊢ v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) ∈ Kᗮ

Tactic:
sub_starProjection_mem_orthogonal (K := K) v

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, setOf, Submodule.sub_starProjection_mem_orthogonal, 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 : E
h : Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) (0 : ↥K)
⊢ v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) ∈ Kᗮ

Tactic:
exact sub_starProjection_mem_orthogonal (K := K) v

Premises used: Submodule.sub_starProjection_mem_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
h : v ∈ Kᗮ
⊢ v - (↑0 : E) ∈ Kᗮ

Tactic:
simpa
-- 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
h : ∀ (x : E), x ∈ (↑K.orthogonalProjection : E →ₗ[𝕜] ↥K).ker ↔ x ∈ Kᗮ
⊢ (↑K.orthogonalProjection : E →ₗ[𝕜] ↥K).ker = Kᗮ

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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
x : E
⊢ x ∈ (↑K.orthogonalProjection : E →ₗ[𝕜] ↥K).ker ↔ x ∈ Kᗮ

Tactic:
orthogonalProjection_eq_zero_iff

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Submodule.orthogonalProjection_eq_zero_iff
-- 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
x : E
⊢ x ∈ (↑K.orthogonalProjection : E →ₗ[𝕜] ↥K).ker ↔ x ∈ Kᗮ

Tactic:
exact orthogonalProjection_eq_zero_iff

Premises used: Submodule.orthogonalProjection_eq_zero_iff
-- 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
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
rw₄ rw₅ :
  (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range = (LinearMap.id - (↑U.starProjection : E →ₗ[𝕜] E)).range
⊢ (↑U.starProjection : E →ₗ[𝕜] E).ker = Uᗮ

Tactic:
rw [LinearMap.IsIdempotentElem.ker_eq_range U.isIdempotentElem_starProjection.toLinearMap,
    ← range_starProjection Uᗮ, starProjection_orthogonal, coe_sub, coe_id]

Premises used: ContinuousLinearMap.IsIdempotentElem.toLinearMap, Submodule.range_starProjection, LinearMap.IsIdempotentElem.ker_eq_range, Submodule.isIdempotentElem_starProjection, Submodule.orthogonal, Submodule.starProjection_orthogonal, ContinuousLinearMap.coe_sub, ContinuousLinearMap.coe_id
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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')

Tactic:
(eq_starProjection_of_mem_of_inner_eq_zero ?_ fun y hy => ?_).symm

Premises used: Submodule.eq_starProjection_of_mem_of_inner_eq_zero, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
refine_1 :
  Membership.mem (α := E') (map f.toLinearMap p) ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E')
refine_2 :
  ∀ (y : E') (hy : y ∈ map f.toLinearMap p),
    ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
          ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
        y⟫ =
      0
⊢ 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')

Tactic:
refine (eq_starProjection_of_mem_of_inner_eq_zero ?_ fun y hy => ?_).symm

Premises used: Submodule.eq_starProjection_of_mem_of_inner_eq_zero, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
⊢ Membership.mem (α := E') (map f.toLinearMap p) ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E')

Tactic:
Submodule.apply_coe_mem_map _ _

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Submodule.apply_coe_mem_map, Classical.choose
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
⊢ Membership.mem (α := E') (map f.toLinearMap p) ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E')

Tactic:
refine Submodule.apply_coe_mem_map _ _

Premises used: Submodule.apply_coe_mem_map
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
y : E'
hy : y ∈ map f.toLinearMap p
refine_2 :
  ∀ (x' : E) (hx' : x' ∈ (↑p : Set E)),
    ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
          ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
        (f : (a : E) → E') x'⟫ =
      0
⊢ ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
        ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
      y⟫ =
    0

Tactic:
rcases hy with ⟨x', hx', rfl : f x' = y⟩

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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 x' : E
hx' : x' ∈ (↑p : Set E)
refine_2 :
  inner.{u_1, u_5} 𝕜 (E := E') ((f : (a : E) → E') (HSub.hSub (β := E) x ((p.starProjection : (a : E) → E) x : E)) : E')
      ((f : (a : E) → E') x' : E') =
    0
refine_2₁ : ⟪HSub.hSub (β := E) x ((p.starProjection : (a : E) → E) x : E), x'⟫ = 0
refine_2₂ refine_2₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪HSub.hSub (α := E') (β := E') ((f : (a : E) → E') x : E')
        ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E'),
      (f : (a : E) → E') x'⟫ =
    0

Tactic:
rw [← f.map_sub, f.inner_map_map, starProjection_inner_eq_zero x x' hx']

Premises used: Submodule.starProjection_inner_eq_zero, LinearIsometry.map_sub, LinearIsometry.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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 :
  HasOrthogonalProjection
    (map
      (↑f : [inst_7 : FunLike (E →ₗᵢ[𝕜] E') E E'] → [SemilinearMapClass (E →ₗᵢ[𝕜] E') (RingHom.id 𝕜) E E'] → E →ₗ[𝕜] E')
      p)
x : E
⊢ Eq.{u_5 + 1} (α := E') ((f : (a : E) → E') ((p.starProjection : (a : E) → E) x : E) : E')
    ((starProjection
            (map
              (↑f :
                [inst_7 : FunLike (E →ₗᵢ[𝕜] E') E E'] →
                  [SemilinearMapClass (E →ₗᵢ[𝕜] E') (RingHom.id 𝕜) E E'] → E →ₗ[𝕜] E')
              p) :
          (a : E') → E')
        ((f : (a : E) → E') x : E') :
      E')

Tactic:
have : (p.map f.toLinearMap).HasOrthogonalProjection := ‹_›
  f.map_starProjection p x

Premises used: SemilinearMapClass.semilinearMap, LinearIsometry.map_starProjection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
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
x : E'
⊢ Eq (α := E') (((map (↑f.toLinearEquiv : E →ₗ[𝕜] E') p).starProjection : (a : E') → E') x : E')
    ((f : (a : E) → E') ((p.starProjection : (a : E) → E) ((f.symm : (a : E') → E) x : E) : E) : E')

Tactic:
simpa only [f.coe_toLinearIsometry, f.apply_symm_apply] using
    (f.toLinearIsometry.map_starProjection' p (f.symm x)).symm

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearIsometryEquiv.symm, LinearIsometryEquiv.apply_symm_apply, LinearIsometry.map_starProjection', LinearIsometryEquiv.coe_toLinearIsometry, Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq.{u_2 + 1} (α := E →L[𝕜] ↥⊥) (orthogonalProjection ⊥) 0

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
rw : Eq.{u_2 + 1} (α := E →L[𝕜] E) (ContinuousLinearMap.comp (M₂ := ↥⊥) (subtypeL ⊥) (orthogonalProjection ⊥)) 0
rw₁ : Eq.{u_2 + 1} (α := E →L[𝕜] E) (ContinuousLinearMap.comp (σ₁₂ := RingHom.id 𝕜) (M₂ := ↥⊥) (subtypeL ⊥) 0) 0
rw₂ rw₃ : Eq.{u_2 + 1} (α := E →L[𝕜] E) 0 0
⊢ Eq.{u_2 + 1} (α := E →L[𝕜] E) (starProjection ⊥) 0

Tactic:
rw [starProjection, orthogonalProjection_bot, ContinuousLinearMap.comp_zero]

Premises used: Submodule.starProjection, Submodule.orthogonalProjection_bot, ContinuousLinearMap.comp_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
⊢ LE.le (α := ℝ) 0 1

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
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
⊢ ‖K.starProjection‖ ≤ 1

Tactic:
K.orthogonalProjection_norm_le

Premises used: ContinuousLinearMap.comp, Submodule.orthogonalProjectionFn, Submodule.starProjection, Set.Mem, setOf, ContinuousLinearMap.opNorm, Submodule.orthogonalProjection, Classical.choose, Submodule.orthogonalProjection_norm_le
-- 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
hv : v ∈ K
⊢ norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) = ‖v‖

Tactic:
congr(‖$(K.starProjection_eq_self_iff.mpr hv)‖)

Premises used: Iff.mpr, Norm.norm, congrArg, id, Submodule.starProjection_eq_self_iff
-- 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
hv : v ∈ K
⊢ norm (E := E) ((K.starProjection : (a : E) → E) v : E) = ‖v‖

Tactic:
norm_orthogonalProjection_apply _ hv

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Submodule.norm_orthogonalProjection_apply, 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 : E
⊢ norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K) ≤ ‖K.orthogonalProjection‖ * ‖v‖

Tactic:
K.orthogonalProjection.le_opNorm _

Premises used: ContinuousLinearMap.le_opNorm, Submodule.orthogonalProjection
-- 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
hbc : ‖K.orthogonalProjection‖ ≤ 1
⊢ ‖K.orthogonalProjection‖ * ‖v‖ ≤ 1 * ‖v‖

Tactic:
gcongr
-- 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.orthogonalProjection‖ ≤ 1

Tactic:
orthogonalProjection_norm_le K

Premises used: Submodule.orthogonalProjection_norm_le
-- 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.orthogonalProjection‖ ≤ 1

Tactic:
exact orthogonalProjection_norm_le K

Premises used: Submodule.orthogonalProjection_norm_le
-- 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
⊢ 1 * ‖v‖ = ‖v‖

Tactic:
simp