Revert "WIP: improve construction of extend; typeclasses fail to be found"

This reverts commit 6eef1526a7bba6ffb597c296bd38bcc10111e435.

Author: grunweg

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative.lean

@@ -434,24 +434,19 @@ The details of the extension are mostly unspecified: for covariant derivatives,
 `s` at points other than `x` will not matter (except for shorter proofs).
 Thus, we choose `s` to be somewhat nice: our chosen construction is linear in `v`.
 -/
-noncomputable def extend [FiniteDimensional ℝ F] [T2Space M] {x : M} (v : V x) :
-    (x' : M) → V x' := by
+noncomputable def extend [FiniteDimensional ℝ F] {x : M} (v : V x) : (x' : M) → V x' :=
   letI b := Basis.ofVectorSpace ℝ F
   letI t := trivializationAt F V x
-  letI V₀ := localExtensionOn b t x v
-  -- Choose a smooth bump function ψ near `x`, supported without t.baseSet
-  -- and return ψ • V₀ instead
-  letI ht := t.open_baseSet.mem_nhds (FiberBundle.mem_baseSet_trivializationAt' x)
-  choose ψ _ hψ using (SmoothBumpFunction.nhds_basis_support (I := I) ht).mem_iff.1 ht
-  exact ψ.toFun • localExtensionOn b t x v
-
--- NB. These two lemmas don't hold for *any* choice of extension of `v`, but they hold for
--- *well-chosen* extensions (such as ours).
+  letI bV := b.localFrame_toBasis_at t (FiberBundle.mem_baseSet_trivializationAt F V x)
+  fun x' ↦ ∑ i, bV.repr v i • b.localFrame t i x'
+
+-- FIXME: these two lemmas only hold for *very particular* choices of extensions of v
+-- (but there exist such choices, and our definition makes these ?! TODO check!!)
 -- so, one may argue this is mathematically wrong, but it encodes the "choice some extension
 -- with this and that property" nicely
 -- a different proof would be to argue only the value at a point matters for cov
 @[simp]
-lemma extend_add_apply [FiniteDimensional ℝ F] [T2Space M] {x : M} (v v' : V x) :
+lemma extend_add_apply [FiniteDimensional ℝ F] {x : M} (v v' : V x) :
     extend F (v + v') = extend F v + extend F v' := by
   ext x
   simp [extend]
@@ -469,29 +464,28 @@ lemma extend_add_apply [FiniteDimensional ℝ F] [T2Space M] {x : M} (v v' : V x
   sorry
 
 @[simp]
-lemma extend_smul_apply [FiniteDimensional ℝ F] [T2Space M] {a : ℝ} (v  : V x) :
+lemma extend_smul_apply [FiniteDimensional ℝ F] {a : ℝ} (v  : V x) :
   extend F (a • v) = a • extend F v := sorry
 
 -- TODO: cleanup this proof by adding simp lemmas to the localFrame stuff
 omit [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] in
-@[simp] lemma extend_apply_self [FiniteDimensional ℝ F] [T2Space M] {x : M} (v : V x) :
+@[simp] lemma extend_apply_self [FiniteDimensional ℝ F] {x : M} (v : V x) :
     extend F v x = v := by
   letI b := Basis.ofVectorSpace ℝ F
   letI t := trivializationAt F V x
   have x_mem : x ∈ t.baseSet := FiberBundle.mem_baseSet_trivializationAt F V x
   letI bV := b.localFrame_toBasis_at t x_mem
-  sorry
-  -- change ∑ i, bV.repr v i • b.localFrame t i x = v
-  -- conv_rhs => rw [←bV.sum_repr v]
-  -- simp [bV, Basis.localFrame_toBasis_at, Basis.localFrame, x_mem]
+  change ∑ i, bV.repr v i • b.localFrame t i x = v
+  conv_rhs => rw [←bV.sum_repr v]
+  simp [bV, Basis.localFrame_toBasis_at, Basis.localFrame, x_mem]
 
-lemma contMDiff_extend [FiniteDimensional ℝ F] [T2Space M] {x : M} (σ₀ : V x) :
+lemma contMDiff_extend [FiniteDimensional ℝ F] {x : M} (σ₀ : V x) :
     ContMDiff I (I.prod 𝓘(ℝ, F)) 1 (fun x ↦ TotalSpace.mk' F x (extend F σ₀ x)) := by
   -- use contMDiffOn_localExtensionOn, plus an abstract result about capping with a bump function
   sorry
 
 /-- The difference of two covariant derivatives, as a tensorial map -/
-noncomputable def difference [FiniteDimensional ℝ F] [T2Space M] [FiniteDimensional ℝ E] [IsManifold I 1 M]
+noncomputable def difference [FiniteDimensional ℝ F] [FiniteDimensional ℝ E] [IsManifold I 1 M]
     (cov cov' : CovariantDerivative I F V) :
     Π x : M, TangentSpace I x → V x → V x :=
   fun x X₀ σ₀ ↦ differenceAux cov cov' (extend E X₀) (extend F σ₀) x
@@ -509,7 +503,7 @@ noncomputable def difference [FiniteDimensional ℝ F] [T2Space M] [FiniteDimens
 
 omit [∀ (x : M), IsTopologicalAddGroup (V x)] [∀ (x : M), ContinuousSMul ℝ (V x)] in
 @[simp]
-lemma difference_apply [FiniteDimensional ℝ F] [IsManifold I 1 M] [T2Space M]
+lemma difference_apply [FiniteDimensional ℝ F] [IsManifold I 1 M]
     (cov cov' : CovariantDerivative I F V) (x : M) (X₀ : TangentSpace I x) (σ₀ : V x) :
     difference cov cov' x X₀ σ₀ =
       cov (extend E X₀) (extend F σ₀) x - cov' (extend E X₀) (extend F σ₀) x := rfl