feat: port Analysis.InnerProductSpace.Projection (#4393)

This PR also increase the priority of `Submodule.bot_ext`. Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>
leanprover-community · May 26, 2023 · 518697a · 518697a
1 parent 60dc12a
commit 518697a
Show file tree

Hide file tree

Showing 3 changed files with 1,380 additions and 1 deletion.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -466,6 +466,7 @@ import Mathlib.Analysis.Hofer
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
 import Mathlib.Analysis.InnerProductSpace.Orthogonal
+import Mathlib.Analysis.InnerProductSpace.Projection
 import Mathlib.Analysis.InnerProductSpace.Symmetric
 import Mathlib.Analysis.LocallyConvex.AbsConvex
 import Mathlib.Analysis.LocallyConvex.BalancedCoreHull

diff --git a/Mathlib/Algebra/Module/Submodule/Lattice.lean b/Mathlib/Algebra/Module/Submodule/Lattice.lean
@@ -95,7 +95,7 @@ protected theorem eq_bot_iff (p : Submodule R M) : p = ⊥ ↔ ∀ x ∈ p, x =
     fun h ↦ eq_bot_iff.mpr fun x hx ↦ (mem_bot R).mpr (h x hx)⟩
 #align submodule.eq_bot_iff Submodule.eq_bot_iff
 
-@[ext]
+@[ext high]
 protected theorem bot_ext (x y : (⊥ : Submodule R M)) : x = y := by
   rcases x with ⟨x, xm⟩; rcases y with ⟨y, ym⟩; congr
   rw [(Submodule.eq_bot_iff _).mp rfl x xm]