bump to nightly-2023-07-24-03

mathlib commit leanprover-community/mathlib@88fcdc3

Archive/All.lean

@@ -53,5 +53,5 @@ import Archive.Wiedijk100Theorems.PerfectNumbers
 import Archive.Wiedijk100Theorems.SolutionOfCubic
 import Archive.Wiedijk100Theorems.SumOfPrimeReciprocalsDiverges
 
-#align_import all from "leanprover-community/mathlib"@"8047de4d911cdef39c2d646165eea972f7f9f539"
+#align_import all from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
 

Counterexamples/All.lean

@@ -13,5 +13,5 @@ import Counterexamples.SeminormLatticeNotDistrib
 import Counterexamples.SorgenfreyLine
 import Counterexamples.ZeroDivisorsInAddMonoidAlgebras
 
-#align_import all from "leanprover-community/mathlib"@"8047de4d911cdef39c2d646165eea972f7f9f539"
+#align_import all from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
 

Mathbin/All.lean

@@ -3212,5 +3212,5 @@ import Mathbin.Topology.VectorBundle.Basic
 import Mathbin.Topology.VectorBundle.Constructions
 import Mathbin.Topology.VectorBundle.Hom
 
-#align_import all from "leanprover-community/mathlib"@"8047de4d911cdef39c2d646165eea972f7f9f539"
+#align_import all from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
 

Mathbin/LinearAlgebra/TensorProduct.lean

@@ -6,7 +6,7 @@ Authors: Kenny Lau, Mario Carneiro
 import Mathbin.GroupTheory.Congruence
 import Mathbin.Algebra.Module.Submodule.Bilinear
 
-#align_import linear_algebra.tensor_product from "leanprover-community/mathlib"@"832f7b9162039c28b9361289c8681f155cae758f"
+#align_import linear_algebra.tensor_product from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
 
 /-!
 # Tensor product of modules over commutative semirings.
@@ -383,7 +383,17 @@ section
 -- Like `R'`, `R'₂` provides a `distrib_mul_action R'₂ (M ⊗[R] N)`
 variable {R'₂ : Type _} [Monoid R'₂] [DistribMulAction R'₂ M]
 
-variable [SMulCommClass R R'₂ M] [SMul R'₂ R']
+variable [SMulCommClass R R'₂ M]
+
+/-- `smul_comm_class R' R'₂ M` implies `smul_comm_class R' R'₂ (M ⊗[R] N)` -/
+instance sMulCommClass_left [SMulCommClass R' R'₂ M] : SMulCommClass R' R'₂ (M ⊗[R] N)
+    where smul_comm r' r'₂ x :=
+    TensorProduct.induction_on x (by simp_rw [TensorProduct.smul_zero])
+      (fun m n => by simp_rw [smul_tmul', smul_comm]) fun x y ihx ihy => by
+      simp_rw [TensorProduct.smul_add]; rw [ihx, ihy]
+#align tensor_product.smul_comm_class_left TensorProduct.sMulCommClass_left
+
+variable [SMul R'₂ R']
 
 #print TensorProduct.isScalarTower_left /-
 /-- `is_scalar_tower R'₂ R' M` implies `is_scalar_tower R'₂ R' (M ⊗[R] N)` -/

Mathbin/RingTheory/TensorProduct.lean

@@ -7,7 +7,7 @@ import Mathbin.LinearAlgebra.FiniteDimensional
 import Mathbin.RingTheory.Adjoin.Basic
 import Mathbin.LinearAlgebra.DirectSum.Finsupp
 
-#align_import ring_theory.tensor_product from "leanprover-community/mathlib"@"69b2e97a276619372b19cf80fc1e91b05ae2baa4"
+#align_import ring_theory.tensor_product from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
 
 /-!
 # The tensor product of R-algebras
@@ -455,19 +455,19 @@ theorem mul_assoc' (mul : A ⊗[R] B →ₗ[R] A ⊗[R] B →ₗ[R] A ⊗[R] B)
 -/
 
 #print Algebra.TensorProduct.mul_assoc /-
-theorem mul_assoc (x y z : A ⊗[R] B) : mul (mul x y) z = mul x (mul y z) :=
+protected theorem mul_assoc (x y z : A ⊗[R] B) : mul (mul x y) z = mul x (mul y z) :=
   mul_assoc' mul (by intros; simp only [mul_apply, mul_assoc]) x y z
 #align algebra.tensor_product.mul_assoc Algebra.TensorProduct.mul_assoc
 -/
 
 #print Algebra.TensorProduct.one_mul /-
-theorem one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x := by
+protected theorem one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x := by
   apply TensorProduct.induction_on x <;> simp (config := { contextual := true })
 #align algebra.tensor_product.one_mul Algebra.TensorProduct.one_mul
 -/
 
 #print Algebra.TensorProduct.mul_one /-
-theorem mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x := by
+protected theorem mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x := by
   apply TensorProduct.induction_on x <;> simp (config := { contextual := true })
 #align algebra.tensor_product.mul_one Algebra.TensorProduct.mul_one
 -/
@@ -485,9 +485,9 @@ instance : Semiring (A ⊗[R] B) :=
     add := (· + ·)
     one := 1
     mul := fun a b => mul a b
-    one_mul := one_mul
-    mul_one := mul_one
-    mul_assoc := mul_assoc
+    one_mul := Algebra.TensorProduct.one_mul
+    mul_one := Algebra.TensorProduct.mul_one
+    mul_assoc := Algebra.TensorProduct.mul_assoc
     zero_mul := by simp
     mul_zero := by simp
     left_distrib := by simp
@@ -530,7 +530,41 @@ def includeLeftRingHom : A →+* A ⊗[R] B
 #align algebra.tensor_product.include_left_ring_hom Algebra.TensorProduct.includeLeftRingHom
 -/
 
-variable {S : Type _} [CommSemiring S] [Algebra S A]
+variable {S : Type _}
+
+-- we want `is_scalar_tower_right` to take priority since it's better for unification elsewhere
+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)
+    apply TensorProduct.induction_on y
+    · simp [smul_zero]
+    · apply TensorProduct.induction_on x
+      · simp [smul_zero]
+      · intro a b a' b'
+        dsimp
+        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, smul_mul_assoc]
+      · intros; simp [smul_add, add_mul, *]
+    · intros; simp [smul_add, mul_add, *]
+#align algebra.tensor_product.is_scalar_tower_right Algebra.TensorProduct.isScalarTower_right
+
+-- we want `algebra.to_smul_comm_class` to take priority since it's better for unification elsewhere
+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
+    apply TensorProduct.induction_on y
+    · simp [smul_zero]
+    · apply TensorProduct.induction_on x
+      · simp [smul_zero]
+      · intro a b a' b'
+        dsimp
+        rw [TensorProduct.smul_tmul', TensorProduct.smul_tmul', tmul_mul_tmul, mul_smul_comm]
+      · intros; simp [smul_add, add_mul, *]
+    · intros; simp [smul_add, mul_add, *]
+#align algebra.tensor_product.smul_comm_class_right Algebra.TensorProduct.sMulCommClass_right
+
+variable [CommSemiring S] [Algebra S A]
 
 #print Algebra.TensorProduct.leftAlgebra /-
 instance leftAlgebra [SMulCommClass R S A] : Algebra S (A ⊗[R] B) :=
@@ -539,16 +573,15 @@ instance leftAlgebra [SMulCommClass R S A] : Algebra S (A ⊗[R] B) :=
       Module S
         (A ⊗[R]
           B)) with
-    commutes' := fun r x => by
-      apply TensorProduct.induction_on x
-      · simp
-      · intro a b; dsimp; rw [Algebra.commutes, _root_.mul_one, _root_.one_mul]
-      · intro y y' h h'; dsimp at h h' ⊢; simp only [mul_add, add_mul, h, h']
-    smul_def' := fun r x => by
-      apply TensorProduct.induction_on x
-      · simp [smul_zero]
-      · intro a b; dsimp; rw [TensorProduct.smul_tmul', Algebra.smul_def r a, _root_.one_mul]
-      · intros; dsimp; simp [smul_add, mul_add, *] }
+    commutes' := fun r x =>
+      by
+      dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply, include_left_ring_hom_apply]
+      rw [algebra_map_eq_smul_one, ← smul_tmul', ← one_def, mul_smul_comm, smul_mul_assoc, mul_one,
+        one_mul]
+    smul_def' := fun r x =>
+      by
+      dsimp only [RingHom.toFun_eq_coe, RingHom.comp_apply, include_left_ring_hom_apply]
+      rw [algebra_map_eq_smul_one, ← smul_tmul', smul_mul_assoc, ← one_def, one_mul] }
 #align algebra.tensor_product.left_algebra Algebra.TensorProduct.leftAlgebra
 -/
 

README.md

@@ -1,4 +1,4 @@
-Tracking mathlib commit: [`8047de4d911cdef39c2d646165eea972f7f9f539`](https://github.com/leanprover-community/mathlib/commit/8047de4d911cdef39c2d646165eea972f7f9f539)
+Tracking mathlib commit: [`88fcdc3da43943f5b01925deddaa5bf0c0e85e4e`](https://github.com/leanprover-community/mathlib/commit/88fcdc3da43943f5b01925deddaa5bf0c0e85e4e)
 
 You should use this repository to inspect the Lean 4 files that `mathport` has generated from mathlib3.
 Please run `lake build` first, to download a copy of the generated `.olean` files.

lake-manifest.json

@@ -10,9 +10,9 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "418039179bc16d9a6e08f19acc1893dd40eee621",
+    "rev": "d6d7a6a2adb17cd0b67778afb8beb4b073c63b67",
     "name": "lean3port",
-    "inputRev?": "418039179bc16d9a6e08f19acc1893dd40eee621"}},
+    "inputRev?": "d6d7a6a2adb17cd0b67778afb8beb4b073c63b67"}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-07-24-01"
+def tag : String := "nightly-2023-07-24-03"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"418039179bc16d9a6e08f19acc1893dd40eee621"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"d6d7a6a2adb17cd0b67778afb8beb4b073c63b67"
 
 @[default_target]
 lean_lib Mathbin where

upstream-rev

@@ -1 +1 @@
-8047de4d911cdef39c2d646165eea972f7f9f539
+88fcdc3da43943f5b01925deddaa5bf0c0e85e4e