From 5ac4fc9295e041af2849679d416f9744393386f4 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Sat, 24 Feb 2024 01:16:02 +0000
Subject: [PATCH] chore: rename arguments to `PiTensorProduct` induction
 principles (#10904)

This looks much nicer in the `induction` tactic than `C1` and `Cp`, as
```lean
induction a using PiTensorProduct.induction_on with
| smul_tprod r a => sorry
| add x y hx hy => sorry
```
---
 Mathlib/LinearAlgebra/PiTensorProduct.lean | 28 ++++++++++++----------
 Mathlib/LinearAlgebra/TensorPower.lean     | 16 ++++++++-----
 2 files changed, 26 insertions(+), 18 deletions(-)

diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean
index 855f8e6d51a4b..8b1df0126792c 100644
--- a/Mathlib/LinearAlgebra/PiTensorProduct.lean
+++ b/Mathlib/LinearAlgebra/PiTensorProduct.lean
@@ -205,17 +205,19 @@ def liftAddHom (φ : (R × Π i, s i) → F)
         (AddCon.ker_rel _).2 <| by simp_rw [AddMonoidHom.map_add, add_comm]
 #align pi_tensor_product.lift_add_hom PiTensorProduct.liftAddHom
 
+/-- Induct using `tprodCoeff` -/
 @[elab_as_elim]
-protected theorem induction_on' {C : (⨂[R] i, s i) → Prop} (z : ⨂[R] i, s i)
-    (C1 : ∀ {r : R} {f : Π i, s i}, C (tprodCoeff R r f)) (Cp : ∀ {x y}, C x → C y → C (x + y)) :
-    C z := by
-  have C0 : C 0 := by
-    have h₁ := @C1 0 0
+protected theorem induction_on' {motive : (⨂[R] i, s i) → Prop} (z : ⨂[R] i, s i)
+    (tprodCoeff : ∀ (r : R) (f : Π i, s i), motive (tprodCoeff R r f))
+    (add : ∀ x y, motive x → motive y → motive (x + y)) :
+    motive z := by
+  have C0 : motive 0 := by
+    have h₁ := tprodCoeff 0 0
     rwa [zero_tprodCoeff] at h₁
   refine' AddCon.induction_on z fun x ↦ FreeAddMonoid.recOn x C0 _
   simp_rw [AddCon.coe_add]
-  refine' fun f y ih ↦ Cp _ ih
-  convert@C1 f.1 f.2
+  refine' fun f y ih ↦ add _ _ _ ih
+  convert tprodCoeff f.1 f.2
 #align pi_tensor_product.induction_on' PiTensorProduct.induction_on'
 
 section DistribMulAction
@@ -324,12 +326,14 @@ theorem tprodCoeff_eq_smul_tprod (z : R) (f : Π i, s i) : tprodCoeff R z f = z
   conv_lhs => rw [this]
 #align pi_tensor_product.tprod_coeff_eq_smul_tprod PiTensorProduct.tprodCoeff_eq_smul_tprod
 
+/-- Induct using scaled versions of `PiTensorProduct.tprod`. -/
 @[elab_as_elim]
-protected theorem induction_on {C : (⨂[R] i, s i) → Prop} (z : ⨂[R] i, s i)
-    (C1 : ∀ {r : R} {f : Π i, s i}, C (r • tprod R f)) (Cp : ∀ {x y}, C x → C y → C (x + y)) :
-    C z := by
-  simp_rw [← tprodCoeff_eq_smul_tprod] at C1
-  exact PiTensorProduct.induction_on' z @C1 @Cp
+protected theorem induction_on {motive : (⨂[R] i, s i) → Prop} (z : ⨂[R] i, s i)
+    (smul_tprod : ∀ (r : R) (f : Π i, s i), motive (r • tprod R f))
+    (add : ∀ x y, motive x → motive y → motive (x + y)) :
+    motive z := by
+  simp_rw [← tprodCoeff_eq_smul_tprod] at smul_tprod
+  exact PiTensorProduct.induction_on' z smul_tprod add
 #align pi_tensor_product.induction_on PiTensorProduct.induction_on
 
 @[ext]
diff --git a/Mathlib/LinearAlgebra/TensorPower.lean b/Mathlib/LinearAlgebra/TensorPower.lean
index 508fe0008137b..144528ce22e93 100644
--- a/Mathlib/LinearAlgebra/TensorPower.lean
+++ b/Mathlib/LinearAlgebra/TensorPower.lean
@@ -169,26 +169,30 @@ variable {R}
 
 theorem one_mul {n} (a : (⨂[R]^n) M) : cast R M (zero_add n) (ₜ1 ₜ* a) = a := by
   rw [gMul_def, gOne_def]
-  induction' a using PiTensorProduct.induction_on with r a x y hx hy
-  · rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
+  induction a using PiTensorProduct.induction_on with
+  | smul_tprod r a =>
+    rw [TensorProduct.tmul_smul, LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
       tprod_mul_tprod, cast_tprod]
     congr 2 with i
     rw [Fin.elim0_append]
     refine' congr_arg a (Fin.ext _)
     simp
-  · rw [TensorProduct.tmul_add, map_add, map_add, hx, hy]
+  | add x y hx hy =>
+    rw [TensorProduct.tmul_add, map_add, map_add, hx, hy]
 #align tensor_power.one_mul TensorPower.one_mul
 
 theorem mul_one {n} (a : (⨂[R]^n) M) : cast R M (add_zero _) (a ₜ* ₜ1) = a := by
   rw [gMul_def, gOne_def]
-  induction' a using PiTensorProduct.induction_on with r a x y hx hy
-  · rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
+  induction a using PiTensorProduct.induction_on with
+  | smul_tprod r a =>
+    rw [← TensorProduct.smul_tmul', LinearEquiv.map_smul, LinearEquiv.map_smul, ← gMul_def,
       tprod_mul_tprod R a _, cast_tprod]
     congr 2 with i
     rw [Fin.append_elim0]
     refine' congr_arg a (Fin.ext _)
     simp
-  · rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
+  | add x y hx hy =>
+    rw [TensorProduct.add_tmul, map_add, map_add, hx, hy]
 #align tensor_power.mul_one TensorPower.mul_one
 
 theorem mul_assoc {na nb nc} (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R]^nc) M) :