chore: register TensorProduct with induction_eliminator (#14204)

eric-wieser · dagurtomas · commit fc2eed61edb4 · 2024-07-02T09:23:22.000Z
Split from #12605
diff --git a/Mathlib/LinearAlgebra/DirectSum/Finsupp.lean b/Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
@@ -101,7 +101,7 @@ lemma finsuppLeft_apply_tmul_apply (p : ι →₀ M) (n : N) (i : ι) :
 
 theorem finsuppLeft_apply (t : (ι →₀ M) ⊗[R] N) (i : ι) :
     finsuppLeft R M N ι t i = rTensor N (Finsupp.lapply i) t := by
-  induction t using TensorProduct.induction_on with
+  induction t with
   | zero => simp
   | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]
   | add x y hx hy => simp [map_add, hx, hy]
@@ -136,7 +136,7 @@ lemma finsuppRight_apply_tmul_apply (m : M) (p : ι →₀ N) (i : ι) :
 
 theorem finsuppRight_apply (t : M ⊗[R] (ι →₀ N)) (i : ι) :
     finsuppRight R M N ι t i = lTensor M (Finsupp.lapply i) t := by
-  induction t using TensorProduct.induction_on with
+  induction t with
   | zero => simp
   | tmul m f => simp [finsuppRight_apply_tmul_apply]
   | add x y hx hy => simp [map_add, hx, hy]
@@ -152,7 +152,7 @@ variable {S : Type*} [CommSemiring S] [Algebra R S]
 
 lemma finsuppLeft_smul' (s : S) (t : (ι →₀ M) ⊗[R] N) :
     finsuppLeft R M N ι (s • t) = s • finsuppLeft R M N ι t := by
-  induction t using TensorProduct.induction_on with
+  induction t with
   | zero => simp
   | add x y hx hy => simp [hx, hy]
   | tmul p n => ext; simp [smul_tmul', finsuppLeft_apply_tmul_apply]
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
@@ -135,7 +135,7 @@ infixl:100 " ⊗ₜ " => tmul _
 notation:100 x " ⊗ₜ[" R "] " y:100 => tmul R x y
 
 -- Porting note: make the arguments of induction_on explicit
-@[elab_as_elim]
+@[elab_as_elim, induction_eliminator]
 protected theorem induction_on {motive : M ⊗[R] N → Prop} (z : M ⊗[R] N)
     (zero : motive 0)
     (tmul : ∀ x y, motive <| x ⊗ₜ[R] y)
@@ -503,7 +503,7 @@ theorem map₂_mk_top_top_eq_top : Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤ :=
 theorem exists_eq_tmul_of_forall (x : TensorProduct R M N)
     (h : ∀ (m₁ m₂ : M) (n₁ n₂ : N), ∃ m n, m₁ ⊗ₜ n₁ + m₂ ⊗ₜ n₂ = m ⊗ₜ[R] n) :
     ∃ m n, x = m ⊗ₜ n := by
-  induction x using TensorProduct.induction_on with
+  induction x with
   | zero =>
     use 0, 0
     rw [TensorProduct.zero_tmul]
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean b/Mathlib/LinearAlgebra/TensorProduct/Finiteness.lean
@@ -51,7 +51,7 @@ namespace TensorProduct
 of `M × N`, such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`. -/
 theorem exists_multiset (x : M ⊗[R] N) :
     ∃ S : Multiset (M × N), x = (S.map fun i ↦ i.1 ⊗ₜ[R] i.2).sum := by
-  induction x using TensorProduct.induction_on with
+  induction x with
   | zero => exact ⟨0, by simp⟩
   | tmul x y => exact ⟨{(x, y)}, by simp⟩
   | add x y hx hy =>
@@ -64,7 +64,7 @@ of `M × N` such that each `m_i` is distinct (we represent it as an element of `
 such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`. -/
 theorem exists_finsupp_left (x : M ⊗[R] N) :
     ∃ S : M →₀ N, x = S.sum fun m n ↦ m ⊗ₜ[R] n := by
-  induction x using TensorProduct.induction_on with
+  induction x with
   | zero => exact ⟨0, by simp⟩
   | tmul x y => exact ⟨Finsupp.single x y, by simp⟩
   | add x y hx hy =>
diff --git a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
@@ -111,7 +111,7 @@ variable (Q) {g}
 theorem LinearMap.lTensor_surjective (hg : Function.Surjective g) :
     Function.Surjective (lTensor Q g) := by
   intro z
-  induction z using TensorProduct.induction_on with
+  induction z with
   | zero => exact ⟨0, map_zero _⟩
   | tmul q p =>
     obtain ⟨n, rfl⟩ := hg p
@@ -136,7 +136,7 @@ theorem LinearMap.lTensor_range :
 theorem LinearMap.rTensor_surjective (hg : Function.Surjective g) :
     Function.Surjective (rTensor Q g) := by
   intro z
-  induction z using TensorProduct.induction_on with
+  induction z with
   | zero => exact ⟨0, map_zero _⟩
   | tmul p q =>
     obtain ⟨n, rfl⟩ := hg p
@@ -532,12 +532,12 @@ lemma Ideal.map_includeLeft_eq (I : Ideal A) :
       use x + y
       simp only [map_add]
     · rintro a x ⟨x, hx, rfl⟩
-      induction a using TensorProduct.induction_on with
+      induction a with
       | zero =>
         use 0
         simp only [map_zero, smul_eq_mul, zero_mul]
       | tmul a b =>
-        induction x using TensorProduct.induction_on with
+        induction x with
         | zero =>
           use 0
           simp only [map_zero, smul_eq_mul, mul_zero]
@@ -557,7 +557,7 @@ lemma Ideal.map_includeLeft_eq (I : Ideal A) :
         simp only [map_add, ha', add_smul, hb']
 
   · rintro x ⟨y, rfl⟩
-    induction y using TensorProduct.induction_on with
+    induction y with
     | zero =>
         rw [map_zero]
         apply zero_mem
@@ -600,12 +600,12 @@ lemma Ideal.map_includeRight_eq (I : Ideal B) :
       use x + y
       simp only [map_add]
     · rintro a x ⟨x, hx, rfl⟩
-      induction a using TensorProduct.induction_on with
+      induction a with
       | zero =>
         use 0
         simp only [map_zero, smul_eq_mul, zero_mul]
       | tmul a b =>
-        induction x using TensorProduct.induction_on with
+        induction x with
         | zero =>
           use 0
           simp only [map_zero, smul_eq_mul, mul_zero]
@@ -625,7 +625,7 @@ lemma Ideal.map_includeRight_eq (I : Ideal B) :
         simp only [map_add, ha', add_smul, hb']
 
   · rintro x ⟨y, rfl⟩
-    induction y using TensorProduct.induction_on with
+    induction y with
     | zero =>
         rw [map_zero]
         apply zero_mem
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean b/Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
@@ -98,7 +98,7 @@ theorem mulMap_eq_mul'_comp_mapIncl : mulMap M N = .mul' R S ∘ₗ TensorProduc
 theorem mulMap_range : LinearMap.range (mulMap M N) = M * N := by
   refine le_antisymm ?_ (mul_le.2 fun m hm n hn ↦ ⟨⟨m, hm⟩ ⊗ₜ[R] ⟨n, hn⟩, rfl⟩)
   rintro _ ⟨x, rfl⟩
-  induction x using TensorProduct.induction_on with
+  induction x with
   | zero => rw [_root_.map_zero]; exact zero_mem _
   | tmul a b => exact mul_mem_mul a.2 b.2
   | add a b ha hb => rw [_root_.map_add]; exact add_mem ha hb
diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean
@@ -422,7 +422,7 @@ theorem exists_fg_le_eq_rTensor_inclusion {R M N : Type*} [CommRing R] [AddCommG
     [AddCommGroup N] [Module R M] [Module R N] {I : Submodule R N} (x : I ⊗ M) :
       ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I) (y : J ⊗ M),
         x = rTensor M (J.inclusion hle) y := by
-  induction x using TensorProduct.induction_on with
+  induction x with
   | zero => exact ⟨⊥, fg_bot, zero_le _, 0, rfl⟩
   | tmul i m => exact ⟨R ∙ i.val, fg_span_singleton i.val,
       (span_singleton_le_iff_mem _ _).mpr i.property,
@@ -733,7 +733,7 @@ instance Module.Finite.base_change [CommSemiring R] [Semiring A] [Algebra R A] [
     obtain ⟨s, hs⟩ := h.out
     refine ⟨⟨s.image (TensorProduct.mk R A M 1), eq_top_iff.mpr ?_⟩⟩
     rintro x -
-    induction x using TensorProduct.induction_on with
+    induction x with
     | zero => exact zero_mem _
     | tmul x y =>
       -- Porting note: new TC reminder
diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean
@@ -117,7 +117,7 @@ theorem IsTensorProduct.inductionOn (h : IsTensorProduct f) {C : M → Prop} (m
   rw [← h.equiv.right_inv m]
   generalize h.equiv.invFun m = y
   change C (TensorProduct.lift f y)
-  induction y using TensorProduct.induction_on with
+  induction y with
   | zero => rwa [map_zero]
   | tmul _ _ =>
     rw [TensorProduct.lift.tmul]
diff --git a/Mathlib/RingTheory/Kaehler/Basic.lean b/Mathlib/RingTheory/Kaehler/Basic.lean
@@ -761,7 +761,7 @@ lemma KaehlerDifferential.range_mapBaseChange :
     LinearMap.range (mapBaseChange R A B) = LinearMap.ker (map R A B B) := by
   apply le_antisymm
   · rintro _ ⟨x, rfl⟩
-    induction' x using TensorProduct.induction_on with r s
+    induction' x with r s
     · simp
     · obtain ⟨x, rfl⟩ := total_surjective _ _ s
       simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]
diff --git a/Mathlib/RingTheory/MatrixAlgebra.lean b/Mathlib/RingTheory/MatrixAlgebra.lean
@@ -122,7 +122,7 @@ theorem right_inv (M : Matrix n n A) : (toFunAlgHom R A n) (invFun R A n M) = M
 #align matrix_equiv_tensor.right_inv MatrixEquivTensor.right_inv
 
 theorem left_inv (M : A ⊗[R] Matrix n n R) : invFun R A n (toFunAlgHom R A n M) = M := by
-  induction M using TensorProduct.induction_on with
+  induction M with
   | zero => simp
   | tmul a m => simp
   | add x y hx hy =>
diff --git a/Mathlib/RingTheory/RingHom/Surjective.lean b/Mathlib/RingTheory/RingHom/Surjective.lean
@@ -37,7 +37,7 @@ theorem surjective_stableUnderBaseChange : StableUnderBaseChange surjective := b
   refine StableUnderBaseChange.mk _ surjective_respectsIso ?_
   classical
   introv h x
-  induction x using TensorProduct.induction_on with
+  induction x with
   | zero => exact ⟨0, map_zero _⟩
   | tmul x y =>
     obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean
@@ -258,9 +258,9 @@ instance (priority := 100) isScalarTower_right [Monoid S] [DistribMulAction S A]
     [IsScalarTower S A A] [SMulCommClass R S A] : IsScalarTower S (A ⊗[R] B) (A ⊗[R] B) where
   smul_assoc r x y := by
     change r • x * y = r • (x * y)
-    induction y using TensorProduct.induction_on with
+    induction y with
     | zero => simp [smul_zero]
-    | tmul a b => induction x using TensorProduct.induction_on with
+    | tmul a b => induction x with
       | zero => simp [smul_zero]
       | tmul a' b' =>
         dsimp
@@ -274,9 +274,9 @@ instance (priority := 100) sMulCommClass_right [Monoid S] [DistribMulAction S A]
     [SMulCommClass S A A] [SMulCommClass R S A] : SMulCommClass S (A ⊗[R] B) (A ⊗[R] B) where
   smul_comm r x y := by
     change r • (x * y) = x * r • y
-    induction y using TensorProduct.induction_on with
+    induction y with
     | zero => simp [smul_zero]
-    | tmul a b => induction x using TensorProduct.induction_on with
+    | tmul a b => induction x with
       | zero => simp [smul_zero]
       | tmul a' b' =>
         dsimp
