Reduce strict defeq compatibility options (#8)

OpenGALib/Riemannian/Instances/EuclideanSpace.lean

@@ -1,5 +1,5 @@
 import Mathlib.Analysis.InnerProductSpace.LinearMap
-import OpenGALib.Riemannian.Metric.RiemannianMetric
+import Mathlib.Geometry.Manifold.Riemannian.Basic
 import OpenGALib.Riemannian.Metric.RiemannianMetric
 
 /-!
@@ -25,33 +25,13 @@ namespace Riemannian
 
 open Bundle Bornology
 open scoped ContDiff Manifold InnerProductSpace
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** The flat metric on a finite-dim inner product space `E`:
 the constant `innerSL ℝ` as bundle-section metric tensor. -/
 noncomputable def euclideanRiemannianMetric
     (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] :
-    RiemannianMetric (𝓘(ℝ, E)) E where
-  inner _ := (innerSL ℝ (E := E) : E →L[ℝ] E →L[ℝ] ℝ)
-  symm _ v w := real_inner_comm _ _
-  pos _ v hv := real_inner_self_pos.2 hv
-  isVonNBounded x := by
-    change IsVonNBounded ℝ {v : E | ⟪v, v⟫_ℝ < 1}
-    have heq : Metric.ball (0 : E) 1 = {v : E | ⟪v, v⟫_ℝ < 1} := by
-      ext v
-      simp only [Metric.mem_ball, dist_zero_right, norm_eq_sqrt_re_inner (𝕜 := ℝ),
-        RCLike.re_to_real, Set.mem_setOf_eq]
-      conv_lhs => rw [show (1 : ℝ) = √1 by simp]
-      rw [Real.sqrt_lt_sqrt_iff]
-      exact real_inner_self_nonneg
-    rw [← heq]
-    exact NormedSpace.isVonNBounded_ball ℝ E 1
-  contMDiff := by
-    intro x
-    rw [contMDiffAt_section]
-    convert contMDiffAt_const (c := innerSL ℝ (E := E))
-    ext v w
-    simp [hom_trivializationAt_apply, ContinuousLinearMap.inCoordinates, TangentSpace]
+    RiemannianMetric (𝓘(ℝ, E)) E :=
+  { riemannianMetricVectorSpace E with
+    contMDiff := (riemannianMetricVectorSpace E).contMDiff.of_le (by exact_mod_cast le_top) }
 
 /-- **Math.** $\langle v, w\rangle_g = \langle v, w\rangle_\mathbb{R}$ on the flat metric. -/
 @[simp]

OpenGALib/Riemannian/Metric/RiemannianMetric.lean

@@ -205,10 +205,10 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
   {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
 
-set_option backward.isDefEq.respectTransparency false in
 instance instFiniteDimensionalTangent [FiniteDimensional ℝ E] (x : M) :
-    FiniteDimensional ℝ (TangentSpace I x) :=
-  inferInstanceAs (FiniteDimensional ℝ E)
+    FiniteDimensional ℝ (TangentSpace I x) := by
+  show FiniteDimensional ℝ E
+  infer_instance
 
 end TangentSpaceInstances
 

OpenGALib/Riemannian/Operators/Hessian.lean

@@ -75,8 +75,6 @@ def IsPointwiseSymm (B : Bilin (M := M) I) : Prop :=
 on $T_x M$. Frobenius and trace against this frame are the **geometric**
 Hilbert-Schmidt norm and trace of $B$ at $x$ (basis-independent among
 $g$-orthonormal frames). -/
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** Frobenius squared norm $\sum_{i,j} B(x)(\varepsilon_i, \varepsilon_j)^2$
 in the $g$-orthonormal frame. -/
 def frobeniusSq (B : Bilin (M := M) I) (x : M) : ℝ :=
@@ -90,8 +88,6 @@ def frobeniusSq (B : Bilin (M := M) I) (x : M) : ℝ :=
         (B x ((stdOrthonormalBasis ℝ (TangentSpace I x)) i : TangentSpace I x)
              ((stdOrthonormalBasis ℝ (TangentSpace I x)) j : TangentSpace I x))^2 :=
   rfl
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** Trace $\sum_i B(x)(\varepsilon_i, \varepsilon_i)$ in the
 $g$-orthonormal frame. -/
 def trace (B : Bilin (M := M) I) (x : M) : ℝ :=
@@ -249,8 +245,6 @@ theorem hessian_eq_mDirDeriv_iterate_sub_chris
   linarith [h_compat]
 
 /-! ## Symmetry of the Hessian on scalar functions -/
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** **Hessian symmetry on scalar functions** (covariant Schwarz / Clairaut):
 $$\mathrm{Hess}\,f(x)(v, w) \;=\; \mathrm{Hess}\,f(x)(w, v).$$
 For $f \in C^2$ near $x$, with $\nabla^M f$ smooth at $x$ as a tangent

OpenGALib/Riemannian/Operators/HessianLie.lean

@@ -338,8 +338,6 @@ private theorem mlieBracket_eq_lieBracketWithin_chart_pullback
   exact (mpullbackWithin_extChartAt_symm_eq_eventually V x).lieBracketWithin_vectorField_eq_of_mem
     (mpullbackWithin_extChartAt_symm_eq_eventually W x)
     (extChartAt_target_subset_range x (mem_extChartAt_target x))
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Manifold scalar Hessian–Lie identity**:
 $D_V(D_W f) - D_W(D_V f) = D_{[V,W]} f$ at $x \in M$, where $D_V f$
 denotes `mfderiv f · (V ·)` and `mlieBracket I V W` is the manifold

OpenGALib/Riemannian/Operators/Laplacian.lean

@@ -92,8 +92,6 @@ The **scalar Laplacian** $\Delta_g f$ of a smooth function $f : M \to \mathbb{R}
 as the trace of the Hessian. Used in the Bochner identity. -/
 
 variable [IsLocallyConstantChartedSpace H M]
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** The **scalar Laplacian** $\Delta_g f(x)$ of a smooth function
 $f : M \to \mathbb{R}$ at $x$, the geometric trace of the Hessian:
 $\Delta_g f(x) = \sum_i \operatorname{Hess} f(x)(\varepsilon_i, \varepsilon_i)$

OpenGALib/Riemannian/Operators/SecondFundamentalForm.lean

@@ -46,7 +46,6 @@ noncomputable def secondFundamentalFormScalar
     (ν X Y : VectorFieldSection I M) (x : M) : ℝ :=
   g.metricInner x (covDeriv g X Y x) (ν x)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** $|A|^2(x) = \sum_{i,j} A(e_i, e_j)^2$ over the standard
 orthonormal basis of `TangentSpace I x`. Basis-independent for
 orthonormal frames. -/
@@ -66,8 +65,6 @@ theorem secondFundamentalFormSqNorm_nonneg
     0 ≤ secondFundamentalFormSqNorm g ν x := by
   unfold secondFundamentalFormSqNorm
   positivity
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** $H(x) = \mathrm{tr}_g A(x) = \sum_i A(e_i, e_i)(x)$. -/
 noncomputable def meanCurvature
     (g : RiemannianMetric I M)

OpenGALib/Riemannian/TangentBundle/TangentSmooth.lean

@@ -308,7 +308,6 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   [IsLocallyConstantChartedSpace H M]
 
 omit [FiniteDimensional ℝ E] [CompleteSpace E] in
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** Smoothness of $y \mapsto \mathrm{d}f_y(v)$ for chart-frame-constant $v$. -/
 theorem mfderiv_const_dir_smoothAt
     {f : M → ℝ} (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) (x : M) (v : E) :
@@ -386,7 +385,6 @@ theorem mfderiv_const_dir_smoothAt
   rfl
 
 omit [FiniteDimensional ℝ E] [CompleteSpace E] in
-set_option backward.isDefEq.respectTransparency false in
 /-- **Math.** Smoothness of $y \mapsto \mathrm{d}f_y(V(y))$ for smoothly-varying $V : M \to E$. -/
 theorem mfderiv_smoothDir_smoothAt
     {f : M → ℝ} (hf : ContMDiff I 𝓘(ℝ, ℝ) ∞ f) {x : M}

OpenGALib/Riemannian/TensorBundle/BundleSectionContinuity.lean

@@ -17,8 +17,6 @@ neighbourhood cover of `chart α source`.
 -/
 
 noncomputable section
-
-set_option backward.isDefEq.respectTransparency false
 set_option linter.style.setOption false
 set_option synthInstance.maxHeartbeats 800000
 set_option maxHeartbeats 800000

OpenGALib/Riemannian/TensorBundle/Defs.lean

@@ -18,6 +18,11 @@ smooth-vector-bundle structure inherited from the tangent bundle.
 namespace Tensor0SBundle
 noncomputable section
 
+-- issue #8: strict `isDefEq` does not synthesize the topology, normed-space,
+-- and `ContMDiffVectorBundle` instances for the tensor-bundle fiber aliases
+-- (`Tensor0SModel`, `TensorRSSpace`, etc.). Keep this option locally to this
+-- foundational tensor-bundle file until those aliases are replaced by explicit
+-- instance bridges.
 set_option backward.isDefEq.respectTransparency false
 
 open Bundle Set IsManifold ContinuousLinearMap

OpenGALib/Riemannian/Util/Chart/ChartJacobianEntries.lean

@@ -27,8 +27,6 @@ The proof identifies the wrapped composition with Mathlib's
 
 noncomputable section
 
-set_option backward.isDefEq.respectTransparency false
-
 open Bundle Set IsManifold ContinuousLinearMap
 open scoped Manifold Topology Bundle ContDiff
 

OpenGALib/Riemannian/Util/Chart/FlatChartDerivs.lean

@@ -29,8 +29,6 @@ smoothness via `inverse` composition). The four public theorems are
 open scoped ContDiff Manifold Topology
 
 namespace TangentBundle
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Eng.** Flat-codomain inverse trivialization: `(trivAt x).symmL ℝ y` retyped
 as `E →L[ℝ] E` via `TangentSpace I y = E`. -/
 noncomputable def symmLFlat
@@ -39,8 +37,6 @@ noncomputable def symmLFlat
     {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
     (x y : M) : E →L[ℝ] E :=
   (trivializationAt E (TangentSpace I) x).symmL ℝ y
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Eng.** Flat-codomain forward chart-mfderiv:
 `(trivAt x₀).continuousLinearMapAt ℝ y` retyped as `E →L[ℝ] E`. -/
 noncomputable def continuousLinearMapAtFlat
@@ -49,8 +45,6 @@ noncomputable def continuousLinearMapAtFlat
     {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
     (x₀ y : M) : E →L[ℝ] E :=
   (trivializationAt E (TangentSpace I) x₀).continuousLinearMapAt ℝ y
-
-set_option backward.isDefEq.respectTransparency false in
 /-- **Eng.** Flat-codomain `mfderivWithin (range I) (extChartAt I x).symm e₀`. -/
 private noncomputable def mfderivWithinFlat
     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
@@ -354,8 +348,6 @@ private theorem mfderivWithinFlat_mdifferentiableWithinAt
       (mfderivWithinFlat x) (extChartAt I x).target (extChartAt I x x) :=
     h_on _ (mem_extChartAt_target x)
   exact h_at_target.mono_of_mem_nhdsWithin (extChartAt_target_mem_nhdsWithin x)
-
-set_option backward.isDefEq.respectTransparency false in
 private theorem symmLFlat_eventuallyEq_mfderivWithinFlat
     {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
     {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}

OpenGALib/Riemannian/Util/CovDeriv/CovDerivSmoothness.lean

@@ -125,7 +125,6 @@ theorem koszulCovDerivAux_tensorialAt
 
 /-! ### Bridge: smoothness of `koszulCovDeriv g X.toFun Y.toFun y` at `x` -/
 
-set_option backward.isDefEq.respectTransparency false in
 /-- **Mixed.** For `X, Y : SmoothVectorField I M`, the section
 `y ↦ koszulCovDeriv g X.toFun Y.toFun y` is `TangentSmoothAt` everywhere.
 

OpenGALib/Riemannian/Util/Metric/CotangentFunctional.lean

@@ -132,7 +132,6 @@ lemma koszulCotangentFunctional_apply
     koszulCotangentFunctional g v Y y w = koszulCotangentScalar g v Y w y := rfl
 
 omit [FiniteDimensional ℝ E] in
-set_option backward.isDefEq.respectTransparency false in
 /-- **Eng.** Scalar smoothness of `koszulCotangentScalar g v Y w` in `y`,
 decomposed across the 6 Koszul terms (3 directional-derivative + 3
 mlieBracket-with-metric-inner). Used to lift `koszulCotangentFunctional` to a

OpenGALib/Riemannian/Util/Tangent/TangentHelpers.lean

@@ -28,7 +28,6 @@ variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E
   [IsLocallyConstantChartedSpace H M]
 
 omit [CompleteSpace E] [FiniteDimensional ℝ E] in
-set_option backward.isDefEq.respectTransparency false in
 /-- **Eng.** A `SmoothVectorField`'s underlying `Y.toFun : Π y : M, T_yM`
 viewed as `M → E` (via `T_yM = E` def-eq) is globally `ContMDiff` under
 `IsLocallyConstantChartedSpace`. Bundle-section ↔ function-form bridge. -/

OpenGALib/Riemannian/Util/Tangent/TensorBundleCoercions.lean

@@ -19,6 +19,11 @@ model representations can `import` this file directly.
 namespace Tensor0SBundle
 noncomputable section
 
+-- issue #8: strict `isDefEq` exposes mismatches between the synthesized
+-- topology/normed-space instances on tensor-bundle fiber aliases and the
+-- instances inferred by the `ContinuousLinearEquiv` coercions below. Keep this
+-- option scoped to the coercion bridge file until those aliases have explicit
+-- topology and CLM coercion lemmas.
 set_option backward.isDefEq.respectTransparency false
 
 open Bundle Set IsManifold ContinuousLinearMap

OpenGALib/Tensor/Multilinear/Fiber.lean

@@ -20,8 +20,6 @@ equivalence to the model fiber.
 
 noncomputable section
 
-set_option backward.isDefEq.respectTransparency false
-
 open Bundle Set
 
 open scoped Manifold Topology Bundle ContDiff BigOperators
@@ -42,8 +40,6 @@ instance instFunLike (s : ℕ) (x : B) :
   ContinuousMultilinearMap.funLike
 
 /-! ## Topology equivalence -/
-
-set_option backward.isDefEq.respectTransparency false in
 /-- The bundle and norm topologies on a `Bundle.continuousMultilinearMap` fiber
 agree. -/
 theorem topology_eq (s : ℕ) (x : B) :
@@ -182,7 +178,8 @@ theorem triv_zero_symmL_apply_elim0 (x₀ x : B)
   have hbase : x ∈ e.baseSet := hx
   have hsymmL : (e.symmL 𝕜 x ω₀ : Bundle.continuousMultilinearMap 𝕜 0 F E x) =
       e.symm x ω₀ := by
-    simp [Trivialization.symmL_apply]
+    rw [Bundle.Trivialization.symmL_apply]
+    rfl
   rw [hsymmL]
   have h1 := triv_zero_apply_eq (F := F) (E := E) x₀ x (e.symm x ω₀) 0
   have h2 : (e ⟨x, e.symm x ω₀⟩ : B × _) = (x, ω₀) :=
@@ -206,7 +203,8 @@ theorem triv_symmL_eq_compContinuousLinearMap {s : ℕ} (x₀ x : B)
   have hbase : x ∈ e.baseSet := hx
   have hsymmL : (e.symmL 𝕜 x T : Bundle.continuousMultilinearMap 𝕜 s F E x) =
       e.symm x T := by
-    simp [Trivialization.symmL_apply]
+    rw [Bundle.Trivialization.symmL_apply]
+    rfl
   rw [hsymmL]
   apply Bundle.continuousMultilinearMap.ext
   intro v

OpenGALib/Tensor/Multilinear/Field.lean

@@ -24,6 +24,11 @@ scalar-function ↔ `0`-multilinear-section equivalence.
 
 noncomputable section
 
+-- issue #8: strict `isDefEq` does not synthesize the
+-- `VectorBundle 𝕜 (ContinuousMultilinearMap 𝕜 (fun _ : Fin s => F) 𝕜)
+--   (Bundle.continuousMultilinearMap 𝕜 s F E)` instance used throughout this
+-- file. Keep the compatibility option at file scope until the multilinear
+-- bundle fiber instances are made explicit enough for strict synthesis.
 set_option backward.isDefEq.respectTransparency false
 
 open Bundle Set

OpenGALib/Tensor/Product/Basis.lean

@@ -101,8 +101,6 @@ coordinate functions (with respect to the tensor product basis) are smooth.
 
 section smooth
 
-set_option backward.isDefEq.respectTransparency false
-
 open Bundle Set
 
 open scoped Manifold Topology Bundle

OpenGALib/Tensor/Product/Bundle.lean

@@ -384,7 +384,6 @@ noncomputable instance memTrivializationAtlas :
     MemTrivializationAtlas
       (e₁.tensorProduct (𝕜 := 𝕜) e₂ :
         Trivialization (F₁ ⊗[𝕜] F₂) (π (F₁ ⊗[𝕜] F₂) (fun x ↦ E₁ x ⊗[𝕜] E₂ x))) := by
-  set_option backward.isDefEq.respectTransparency false in
   letI : (b : B) → TopologicalSpace (E₁ b ⊗[𝕜] E₂ b) := fun b ↦ inferInstance
   exact ⟨_, ⟨e₁, e₂, he₁, he₂, rfl⟩, rfl⟩
 

OpenGALib/Tensor/Product/Section.lean

@@ -27,8 +27,6 @@ tensor product, smooth section, vector bundle
 
 noncomputable section
 
-set_option backward.isDefEq.respectTransparency false
-
 open Bundle Set
 
 open scoped Manifold Topology Bundle TensorProduct