From e718fd1b97d8eebb3c45c679f0a2729ba35231f1 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Sat, 25 Apr 2026 19:54:55 +0800 Subject: [PATCH 1/2] chore(Analysis/InnerProductSpace/Projection/Basic): remove an erw --- Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index 2a4295c0506c80..4f55678e0725b4 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -71,7 +71,7 @@ instance HasOrthogonalProjection.map_linearIsometryEquiv [K.HasOrthogonalProject exists_orthogonal v := by rcases HasOrthogonalProjection.exists_orthogonal (K := K) (f.symm v) with ⟨w, hwK, hw⟩ refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩ - erw [← f.symm.inner_map_map, f.symm_apply_apply, map_sub, f.symm_apply_apply, hw u hu] + simp [← f.symm.inner_map_map, map_sub, hw u hu] instance HasOrthogonalProjection.map_linearIsometryEquiv' [K.HasOrthogonalProjection] {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') : From 43ca67bd7c95c5f08eb0529dac8e628e0e86ec54 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 25 Apr 2026 20:06:41 +0800 Subject: [PATCH 2/2] Update Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com> --- Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean index 4f55678e0725b4..3cae48ca82f6c4 100644 --- a/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean +++ b/Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean @@ -71,7 +71,7 @@ instance HasOrthogonalProjection.map_linearIsometryEquiv [K.HasOrthogonalProject exists_orthogonal v := by rcases HasOrthogonalProjection.exists_orthogonal (K := K) (f.symm v) with ⟨w, hwK, hw⟩ refine ⟨f w, Submodule.mem_map_of_mem hwK, Set.forall_mem_image.2 fun u hu ↦ ?_⟩ - simp [← f.symm.inner_map_map, map_sub, hw u hu] + simp [← f.symm.inner_map_map, hw u hu] instance HasOrthogonalProjection.map_linearIsometryEquiv' [K.HasOrthogonalProjection] {E' : Type*} [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') :