chore(LinearAlgebra.TensorAlgebra): more idiomatic transparency management in induction (#31953)

Normally to contain reduction at weaker transparency we build the appropriate
API via theorems. Here we have a `let` definition. We could factor it out and
proceed as usual but that does not seem worth the effort currently. So we mimic
this with a `have` instead.

Co-authored-by: Matthew Ballard <[email protected]>

Author: mattrobball

Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean

@@ -191,13 +191,11 @@ theorem induction {C : TensorAlgebra R M → Prop}
       add_mem' := @add
       algebraMap_mem' := algebraMap }
   let of : M →ₗ[R] s := (TensorAlgebra.ι R).codRestrict (Subalgebra.toSubmodule s) ι
+  have of_apply {x : M} : of x = (TensorAlgebra.ι R) x := by rfl
   -- the mapping through the subalgebra is the identity
   have of_id : AlgHom.id R (TensorAlgebra R M) = s.val.comp (lift R of) := by
     ext
-    simp only [AlgHom.toLinearMap_id, LinearMap.id_comp, AlgHom.comp_toLinearMap,
-      LinearMap.coe_comp, Function.comp_apply, AlgHom.toLinearMap_apply, lift_ι_apply,
-      Subalgebra.coe_val]
-    erw [LinearMap.codRestrict_apply]
+    simp [of_apply]
   -- finding a proof is finding an element of the subalgebra
   rw [← AlgHom.id_apply (R := R) a, of_id]
   exact Subtype.prop (lift R of a)