chore(algebra/algebra/operations): add missing `@[elab_as_eliminator]…

…` on recursors (#12440)

`refine submodule.pow_induction_on' _ _ _ _ h` struggles without this attribute

src/algebra/algebra/operations.lean

@@ -336,7 +336,7 @@ begin
 end
 
 /-- Dependent version of `submodule.pow_induction_on`. -/
-protected theorem pow_induction_on'
+@[elab_as_eliminator] protected theorem pow_induction_on'
   {C : Π (n : ℕ) x, x ∈ M ^ n → Prop}
   (hr : ∀ r : R, C 0 (algebra_map _ _ r) (algebra_map_mem r))
   (hadd : ∀ x y i hx hy, C i x hx → C i y hy → C i (x + y) (add_mem _ ‹_› ‹_›))
@@ -354,7 +354,7 @@ end
 
 /-- To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars,
 is closed under addition, and holds for `m * x` where `m ∈ M` and it holds for `x` -/
-protected theorem pow_induction_on
+@[elab_as_eliminator] protected theorem pow_induction_on
   {C : A → Prop}
   (hr : ∀ r : R, C (algebra_map _ _ r))
   (hadd : ∀ x y, C x → C y → C (x + y))

src/linear_algebra/exterior_algebra/grading.lean

@@ -56,7 +56,7 @@ graded_algebra.of_alg_hom _
   (λ i x, begin
     cases x with x hx,
     dsimp only [subtype.coe_mk, direct_sum.lof_eq_of],
-    apply submodule.pow_induction_on' _
+    refine submodule.pow_induction_on' _
       (λ r, _) (λ x y i hx hy ihx ihy, _) (λ m hm i x hx ih, _) hx,
     { rw [alg_hom.commutes, direct_sum.algebra_map_apply], refl },
     { rw [alg_hom.map_add, ihx, ihy, ←map_add], refl },

src/linear_algebra/tensor_algebra/grading.lean

@@ -47,7 +47,7 @@ graded_algebra.of_alg_hom _
   (λ i x, begin
     cases x with x hx,
     dsimp only [subtype.coe_mk, direct_sum.lof_eq_of],
-    apply submodule.pow_induction_on' _
+    refine submodule.pow_induction_on' _
       (λ r, _) (λ x y i hx hy ihx ihy, _) (λ m hm i x hx ih, _) hx,
     { rw [alg_hom.commutes, direct_sum.algebra_map_apply], refl },
     { rw [alg_hom.map_add, ihx, ihy, ←map_add], refl },