awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
⊢ ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε

Tactic:
⟨I, fun i (hi : I ≤ i) => ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
intro : ∀ (i : ι) (hi : I ≤ i), ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε
⊢ ∃ (I : ι), ∀ i ≥ I, ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε

Tactic:
refine ⟨I, fun i (hi : I ≤ i) => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
intro : ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ < ε
⊢ ‖HSub.hSub (α := E) (((U i).starProjection : (a : E) → E) y : E) y‖ < ε

Tactic:
rw [norm_sub_rev, starProjection_minimal]

Premises used: Submodule.starProjection_minimal, norm_sub_rev
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ < ε

Tactic:
lt_of_le_of_lt ?_ hay

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
intro : ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ ≤ ‖y - a‖
⊢ ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ < ε

Tactic:
refine lt_of_le_of_lt ?_ hay

Premises used: lt_of_le_of_lt
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
intro : ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ ≤ ‖y - (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U i) a ⋯) : E)‖
⊢ ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ ≤ ‖y - a‖

Tactic:
change _ ≤ ‖y - (⟨a, hU hi hI⟩ : U i)‖

Premises used: Subtype.mk
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ ≤ ‖y - (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U i) a ⋯) : E)‖

Tactic:
ciInf_le ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ _

Premises used: Iff.mpr, Set.forall_mem_range, ciInf_le, Exists.intro, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (i : ι), (U i).HasOrthogonalProjection
inst_5 : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
hU : Monotone U
x : E
h : NeBot.{u_4} (α := ι) atTop
left : Nonempty ι
right : IsDirectedOrder ι
y : E := (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
proj_x :
  ∀ (i : ι),
    Eq (α := ↥(U i)) (((U i).orthogonalProjection : (a : E) → ↥(U i)) x : ↥(U i))
      (((U i).orthogonalProjection : (a : E) → ↥(U i)) y : ↥(U i))
ε : ℝ
hε : ε > 0
a : E
ha : Membership.mem (γ := Submodule 𝕜 E) (⨆ (i : ι), U i) a
hay : ‖y - a‖ < ε
I : ι
hI : a ∈ U I
i : ι
hi : I ≤ i
⊢ ⨅ (x : ↥(U i)), ‖y - (↑x : E)‖ ≤ ‖y - (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ U i) a ⋯) : E)‖

Tactic:
exact ciInf_le ⟨0, Set.forall_mem_range.mpr fun _ => norm_nonneg _⟩ _

Premises used: Iff.mpr, Set.forall_mem_range, ciInf_le, Exists.intro, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
rw : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) ⊤
⊢ HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))

Tactic:
rw [top_unique hU']

Premises used: top_unique
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
⊢ HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) ⊤

Tactic:
infer_instance
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
⊢ HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))

Tactic:
have : (⨆ i, U i).topologicalClosure.HasOrthogonalProjection := by
    rw [top_unique hU']
    infer_instance
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
this : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
⊢ Tendsto (β := E) (fun (i : ι) ↦ (((U i).starProjection : (a : E) → E) x : E)) atTop
    (𝓝 ((starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x) : Filter E)

Tactic:
starProjection_tendsto_closure_iSup U hU x

Premises used: Submodule.starProjection_tendsto_closure_iSup
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
this : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
h : x = (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x
⊢ Tendsto (fun (t : ι) ↦ ((U t).starProjection : (a : E) → E) x) atTop (𝓝 x)

Tactic:
convert! starProjection_tendsto_closure_iSup U hU x

Premises used: Submodule.starProjection_tendsto_closure_iSup
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
this : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
h : Membership.mem (γ := Submodule 𝕜 E) ⊤ x
⊢ x = (starProjection (topologicalClosure (⨆ (i : ι), U i)) : (a : E) → E) x

Tactic:
rw [eq_comm, starProjection_eq_self_iff, top_unique hU']

Premises used: eq_comm, top_unique, Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
ι : Type u_4
inst_3 : Preorder ι
U : ι → Submodule 𝕜 E
inst_4 : ∀ (t : ι), (U t).HasOrthogonalProjection
hU : Monotone U
x : E
hU' : LE.le.{u_2} (α := Submodule 𝕜 E) ⊤ (topologicalClosure (⨆ (t : ι), U t))
this : HasOrthogonalProjection.{u_1, u_2} (𝕜 := 𝕜) (E := E) (topologicalClosure (⨆ (i : ι), U i))
⊢ Membership.mem (γ := Submodule 𝕜 E) ⊤ x

Tactic:
trivial
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
⊢ Kᗮᗮᗮ = Kᗮ

Tactic:
(orthogonal_gc 𝕜 E).u_l_u_eq_u K

Premises used: Submodule.orthogonal_gc, GaloisConnection.u_l_u_eq_u
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
rw : Kᗮᗮ = ⊤ ↔ Kᗮ = ⊥
⊢ K.topologicalClosure = ⊤ ↔ Kᗮ = ⊥

Tactic:
rw [← K.orthogonal_orthogonal_eq_closure]

Premises used: Submodule.orthogonal_orthogonal_eq_closure
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
mp : Kᗮᗮ = ⊤ → Kᗮ = ⊥
mpr : Kᗮ = ⊥ → Kᗮᗮ = ⊤
⊢ Kᗮᗮ = ⊤ ↔ Kᗮ = ⊥

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
h : Kᗮᗮ = ⊤
mp : Kᗮᗮᗮ = ⊥
mp₁ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ᗮ ⊥
mp₂ mp₃ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ ⊥
⊢ Kᗮ = ⊥

Tactic:
rw [← Submodule.triorthogonal_eq_orthogonal, h, Submodule.top_orthogonal_eq_bot]

Premises used: Submodule.top_orthogonal_eq_bot, Submodule.triorthogonal_eq_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : CompleteSpace E
h : Kᗮ = ⊥
mpr : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊥ᗮ ⊤
mpr₁ mpr₂ : Eq.{u_2 + 1} (α := Submodule 𝕜 E) ⊤ ⊤
⊢ Kᗮᗮ = ⊤

Tactic:
rw [h, Submodule.bot_orthogonal_eq_top]

Premises used: Submodule.bot_orthogonal_eq_top
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
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
⊢ IsCompl K Kᗮ

Tactic:
have : IsCompl K Kᗮ := Submodule.isCompl_orthogonal_of_hasOrthogonalProjection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
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
this : IsCompl K Kᗮ
rw :
  ((K.orthogonalProjection : (a : E) → ↥K)
      (HAdd.hAdd (α := E) (β := E) ((K.projection Kᗮ this : (a : E) → E) x : E)
        ((Kᗮ.projection K ⋯ : (a : E) → E) x : E)) :
    ↥K)
| ((K.orthogonalProjection : (a : E) → ↥K) x : ↥K)

Tactic:
rw [← projection_add_projection_eq_self this x]

Premises used: Submodule.projection_add_projection_eq_self
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
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
this : IsCompl K Kᗮ
conv_lhs :
  Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (β := E) ((K.projection Kᗮ this : (a : E) → E) x : E)
          ((Kᗮ.projection K ⋯ : (a : E) → E) x : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
⊢ Eq (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) x : ↥K) ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)

Tactic:
conv_lhs => rw [← projection_add_projection_eq_self this x]

Premises used: Submodule.projection_add_projection_eq_self
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
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
this : IsCompl K Kᗮ
simp_rw :
  Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E)
          (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
⊢ Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (β := E) ((K.projection Kᗮ this : (a : E) → E) x : E)
          ((Kᗮ.projection K ⋯ : (a : E) → E) x : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)

Tactic:
simp_rw [projection_apply]

Premises used: Submodule.projection_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
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
this : IsCompl K Kᗮ
rw :
  HAdd.hAdd (α := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E))
      ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
rw₁ :
  HAdd.hAdd (α := ↥K) (β := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K)
      ((K.orthogonalProjection : (a : E) → ↥K) (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E) : ↥K) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
rw₂ :
  HAdd.hAdd (α := ↥K) (β := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K) (0 : ↥K) =
    (K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x
rw₃ rw₄ :
  Eq (α := ↥K) ((K.projectionOnto Kᗮ this : (a : E) → ↥K) x : ↥K) ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)
⊢ Eq (α := ↥K)
    ((K.orthogonalProjection : (a : E) → ↥K)
        (HAdd.hAdd (α := E) (↑((K.projectionOnto Kᗮ this : (a : E) → ↥K) x) : E)
          (↑((Kᗮ.projectionOnto K ⋯ : (a : E) → ↥Kᗮ) x) : E)) :
      ↥K)
    ((K.projectionOnto Kᗮ ⋯ : (a : E) → ↥K) x : ↥K)

Tactic:
rw [map_add, orthogonalProjection_mem_subspace_eq_self,
    orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]

Premises used: Submodule.orthogonalProjection_mem_subspace_eq_self, Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, map_add, Submodule.coe_mem, add_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
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) = K.projectionOnto Kᗮ ⋯

Tactic:
LinearMap.ext orthogonalProjection_apply_eq_linearProjOfIsCompl

Premises used: LinearMap.ext, Submodule.orthogonalProjection_apply_eq_linearProjOfIsCompl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
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 : E →ₗ[𝕜] E) = K.projection Kᗮ ⋯

Tactic:
simp [starProjection, toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl, projection]

Premises used: Submodule.projection, Submodule.starProjection, Submodule.toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
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
⊢ Eq (α := E) ((K.starProjection : (a : E) → E) x : E) ((K.projection Kᗮ ⋯ : (a : E) → E) x : E)

Tactic:
congr($toLinearMap_starProjection_eq_isComplProjection x)

Premises used: congrArg, Submodule.toLinearMap_starProjection_eq_isComplProjection, id, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x : E
hK : Dense (↑K : Set E)
h : x ∈ Kᗮ
⊢ x = 0

Tactic:
eq_zero_of_inner_left 𝕜 hK fun _ ↦ (mem_orthogonal' _ _).1 h _

Premises used: Submodule.mem_orthogonal', Iff.mp, Dense.eq_zero_of_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
x y : E
hK : Dense (↑K : Set E)
h : x - y ∈ Kᗮ
⊢ x = y

Tactic:
sub_eq_zero.1 <| eq_zero_of_mem_orthogonal hK h

Premises used: sub_eq_zero, Dense.eq_zero_of_mem_orthogonal, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
inst_3 : (↑K : Submodule 𝕜 E).HasOrthogonalProjection
carrier : ∀ (x : E), x ∈ (↑Kᗮᗮ : Submodule 𝕜 E).carrier ↔ x ∈ (↑K : Submodule 𝕜 E).carrier
⊢ Kᗮᗮ = K

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : ClosedSubmodule 𝕜 E
inst_3 : (↑K : Submodule 𝕜 E).HasOrthogonalProjection
x : E
⊢ x ∈ (↑Kᗮᗮ : Submodule 𝕜 E).carrier ↔ x ∈ (↑K : Submodule 𝕜 E).carrier

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : ClosedSubmodule 𝕜 E
inst_3 : (↑K₁ : Submodule 𝕜 E).HasOrthogonalProjection
inst_4 : (↑K₂ : Submodule 𝕜 E).HasOrthogonalProjection
h : K₁ᗮ = K₂ᗮ
⊢ K₁ = K₂

Tactic:
simpa using congr($hᗮ)
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
⊢ Function.Injective (β := ClosedSubmodule 𝕜 E) fun (K : ClosedSubmodule 𝕜 E) ↦ Kᗮ

Tactic:
(orthogonal_eq_orthogonal_iff · · |>.mp)

Premises used: ClosedSubmodule.orthogonal_eq_orthogonal_iff, Iff.mp, Function.Injective
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Submodule
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
K₁ K₂ : ClosedSubmodule 𝕜 E
⊢ K₁ᗮ ⊔ K₂ᗮ = (K₁ ⊓ K₂)ᗮ

Tactic:
simpa using congr($(inf_orthogonal K₁ᗮ K₂ᗮ)ᗮ).symm

Premises used: ClosedSubmodule.inf_orthogonal, congrArg, id, ClosedSubmodule.orthogonal, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
pos : ∀ (hx : x = 0), T.rayleighQuotient (c • x) = T.rayleighQuotient x
neg : ∀ (hx : ¬x = 0), T.rayleighQuotient (c • x) = T.rayleighQuotient x
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
simp [hx]
-- Module: Mathlib.Analysis.InnerProductSpace.Rayleigh
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
hc : c ≠ 0
hx : ¬x = 0
⊢ T.rayleighQuotient (c • x) = T.rayleighQuotient x

Tactic:
simp [field, norm_smul, T.reApplyInnerSelf_smul]

Premises used: norm_smul, ContinuousLinearMap.reApplyInnerSelf_smul