Eliminate set_option backward.isDefEq.respectTransparency false workarounds

[Xinze-Li-Moqian]

Background

Lean 4 is migrating to strict isDefEq that respects transparency settings. Mathlib code that relied on lax defeq (auto-unfolding non-reducible defs during instance synthesis) needs adjustment. The option

```lean
set_option backward.isDefEq.respectTransparency false in
instance foo : ... := ...
```

is a compatibility escape hatch that disables strict mode for one declaration. It is not a permanent fix.

Status in OpenGA

The original Metric/RiemannianMetric.lean :: instFiniteDimensionalTangent had this workaround. Fixed in commit e1da355 by switching to

```lean
instance ... := by show FiniteDimensional ℝ E; infer_instance
```

The show tactic forces whnf unfolding (which IS aggressive enough) without disabling transparency-respect globally.

Remaining occurrences

```
$ grep -rln "set_option backward.isDefEq.respectTransparency false" OpenGALib/
```

Expected hits (TBD by running):

• OpenGALib/Riemannian/Util/ChartJacobianSmoothness.lean
• (others — need to enumerate)

Plan

For each occurrence:

1. Identify the synthesis goal that needs unfolding.
2. Try show <expected_type> + infer_instance / exact ....
3. If that fails, try explicit unfold then resume.
4. If neither works, document why (might be a real upstream Mathlib gap).

Acceptance

• Zero set_option backward.isDefEq.respectTransparency false remain in OpenGA, OR each remaining one has a code comment explaining why it's irreducible.
• Build clean.

See also

• Mathlib/Tactic/DefEqAbuse.lean — #defeq_abuse diagnostic tactic.