[Merged by Bors] - feat: continuousLinearMapAt_apply_of_mem

Mathlib/Geometry/Manifold/Riemannian/Basic.lean

@@ -121,8 +121,7 @@ noncomputable def riemannianMetricVectorSpace :
     rw [contMDiffAt_section]
     convert contMDiffAt_const (c := innerSL ℝ)
     ext v w
-    simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates,
-      Trivialization.linearMapAt_apply, TangentSpace]
+    simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates, TangentSpace]
 
 noncomputable instance : RiemannianBundle (fun (x : F) ↦ TangentSpace 𝓘(ℝ, F) x) :=
   ⟨(riemannianMetricVectorSpace F).toRiemannianMetric⟩

Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean

@@ -103,7 +103,7 @@ instance : IsContMDiffRiemannianBundle IB n F₁ (Bundle.Trivial B F₁) := by
   simp only [contMDiffAt_section]
   convert contMDiffAt_const (c := innerSL ℝ)
   ext v w
-  simp [hom_trivializationAt_apply, inCoordinates, Trivialization.linearMapAt_apply]
+  simp [hom_trivializationAt_apply, inCoordinates]
 
 end Trivial
 

Mathlib/Topology/VectorBundle/Basic.lean

@@ -121,6 +121,7 @@ theorem coe_linearMapAt (e : Pretrivialization F (π F E)) [e.IsLinear R] (b : B
   rw [Pretrivialization.linearMapAt]
   split_ifs <;> rfl
 
+@[simp]
 theorem coe_linearMapAt_of_mem (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B}
     (hb : b ∈ e.baseSet) : ⇑(e.linearMapAt R b) = fun y => (e ⟨b, y⟩).2 := by
   simp_rw [coe_linearMapAt, if_pos hb]
@@ -143,14 +144,10 @@ theorem linearMapAt_eq_zero (e : Pretrivialization F (π F E)) [e.IsLinear R] {b
   dif_neg hb
 
 theorem symmₗ_linearMapAt (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B}
-    (hb : b ∈ e.baseSet) (y : E b) : e.symmₗ R b (e.linearMapAt R b y) = y := by
-  rw [e.linearMapAt_def_of_mem hb]
-  exact (e.linearEquivAt R b hb).left_inv y
+    (hb : b ∈ e.baseSet) (y : E b) : e.symmₗ R b (e.linearMapAt R b y) = y := by simp [hb]
 
 theorem linearMapAt_symmₗ (e : Pretrivialization F (π F E)) [e.IsLinear R] {b : B}
-    (hb : b ∈ e.baseSet) (y : F) : e.linearMapAt R b (e.symmₗ R b y) = y := by
-  rw [e.linearMapAt_def_of_mem hb]
-  exact (e.linearEquivAt R b hb).right_inv y
+    (hb : b ∈ e.baseSet) (y : F) : e.linearMapAt R b (e.symmₗ R b y) = y := by simp [hb]
 
 end Pretrivialization
 
@@ -214,6 +211,7 @@ theorem coe_linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) :
     ⇑(e.linearMapAt R b) = fun y => if b ∈ e.baseSet then (e ⟨b, y⟩).2 else 0 :=
   e.toPretrivialization.coe_linearMapAt b
 
+@[simp]
 theorem coe_linearMapAt_of_mem (e : Trivialization F (π F E)) [e.IsLinear R] {b : B}
     (hb : b ∈ e.baseSet) : ⇑(e.linearMapAt R b) = fun y => (e ⟨b, y⟩).2 := by
   simp_rw [coe_linearMapAt, if_pos hb]
@@ -231,7 +229,6 @@ theorem linearMapAt_def_of_notMem (e : Trivialization F (π F E)) [e.IsLinear R]
     (hb : b ∉ e.baseSet) : e.linearMapAt R b = 0 :=
   dif_neg hb
 
-@[simp]
 theorem symm_linearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] {b : B} (hb : b ∈ e.baseSet)
     (y : E b) : e.symm b (e.linearMapAt R b y) = y :=
   e.toPretrivialization.symmₗ_linearMapAt hb y
@@ -392,6 +389,11 @@ def continuousLinearMapAt (e : Trivialization F (π F E)) [e.IsLinear R] (b : B)
       exact (e.continuousOn.comp_continuous (FiberBundle.totalSpaceMk_isInducing F E b).continuous
         fun x => e.mem_source.mpr hb).snd }
 
+lemma continuousLinearMapAt_apply_of_mem (e : Trivialization F TotalSpace.proj)
+    [Trivialization.IsLinear R e] {b : B} (hb : b ∈ e.baseSet) (y : E b) :
+    (continuousLinearMapAt R e b) y = (e ⟨b, y⟩).2 := by
+  simp [coe_linearMapAt_of_mem e hb]
+
 /-- Backwards map of `Bundle.Trivialization.continuousLinearEquivAt`, defined everywhere. -/
 @[simps -fullyApplied apply]
 def symmL (e : Trivialization F (π F E)) [e.IsLinear R] (b : B) : F →L[R] E b :=
@@ -708,8 +710,8 @@ variable {i j}
 theorem localTriv_continuousLinearMapAt {b : B} (hb : b ∈ (Z.localTriv i).baseSet) :
     (Z.localTriv i).continuousLinearMapAt R b = Z.coordChange (Z.indexAt b) i b := by
   ext1 v
-  rw [(Z.localTriv i).continuousLinearMapAt_apply R, (Z.localTriv i).coe_linearMapAt_of_mem]
-  exacts [rfl, hb]
+  simp_all
+  rfl
 
 @[simp, mfld_simps]
 theorem trivializationAt_continuousLinearMapAt {b₀ b : B}

Mathlib/Topology/VectorBundle/Riemannian.lean

@@ -80,7 +80,7 @@ instance : IsContinuousRiemannianBundle F₁ (Bundle.Trivial B F₁) := by
   refine ⟨continuousAt_id, ?_⟩
   convert continuousAt_const (y := innerSL ℝ)
   ext v w
-  simp [hom_trivializationAt_apply, inCoordinates, Trivialization.linearMapAt_apply]
+  simp [hom_trivializationAt_apply, inCoordinates]
 
 end Trivial
 
@@ -189,8 +189,7 @@ lemma eventually_norm_symmL_trivializationAt_self_comp_lt (x : B) {r : ℝ} (hr
     have A : ((trivializationAt F E x).symm y)
        ((trivializationAt F E x).linearMapAt ℝ y v) = v := by
       convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'y).symm_apply_apply v
-      rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'y]
-      rfl
+      simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'y]
     simp [A, w]
   have hgx : g x ((trivializationAt F E x).symm x w) ((trivializationAt F E x).symm x w) =
       g' x w w := by
@@ -232,8 +231,7 @@ lemma eventually_norm_trivializationAt_lt (x : B) :
     simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
       Function.comp_apply, coe_id', id_eq]
     convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
-    rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
-    rfl
+    simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
   have : (trivializationAt F E x).continuousLinearMapAt ℝ y =
     (ContinuousLinearMap.id _ _) ∘L ((trivializationAt F E x).continuousLinearMapAt ℝ y) := by simp
   grw [this, ← A, comp_assoc, opNorm_comp_le]
@@ -294,8 +292,7 @@ lemma eventually_norm_symmL_trivializationAt_comp_self_lt (x : B) {r : ℝ} (hr
     have A : ((trivializationAt F E x).symm x)
        ((trivializationAt F E x).linearMapAt ℝ x v) = v := by
       convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).symm_apply_apply v
-      rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
-      rfl
+      simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
     simp [A, w]
   have hgy : g y ((trivializationAt F E x).symm y w) ((trivializationAt F E x).symm y w)
       = g' y w w := by
@@ -339,8 +336,7 @@ lemma eventually_norm_symmL_trivializationAt_lt (x : B) :
     simp only [coe_comp', Trivialization.continuousLinearMapAt_apply, Trivialization.symmL_apply,
       Function.comp_apply, coe_id', id_eq]
     convert ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).apply_symm_apply v
-    rw [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
-    rfl
+    simp [Trivialization.coe_continuousLinearEquivAt_eq _ h'x]
   have : (trivializationAt F E x).symmL ℝ y =
      ((trivializationAt F E x).symmL ℝ y) ∘L (ContinuousLinearMap.id _ _) := by simp
   grw [this, ← A, ← comp_assoc, opNorm_comp_le]