chore: minor backports from nightly-testing (#12531)

Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · May 12, 2024 · 2134833 · 2134833
1 parent fe44e01
commit 2134833
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 6 deletions.
diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean
@@ -389,6 +389,7 @@ abbrev shiftAdd (i j : A) : X⟦i + j⟧ ≅ X⟦i⟧⟦j⟧ :=
 theorem shift_shift' (i j : A) :
     f⟦i⟧'⟦j⟧' = (shiftAdd X i j).inv ≫ f⟦i + j⟧' ≫ (shiftAdd Y i j).hom := by
   symm
+  rw [← Functor.comp_map, NatIso.app_inv]
   apply NatIso.naturality_1
 #align category_theory.shift_shift' CategoryTheory.shift_shift'
 
@@ -401,6 +402,7 @@ abbrev shiftZero : X⟦(0 : A)⟧ ≅ X :=
 
 theorem shiftZero' : f⟦(0 : A)⟧' = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv := by
   symm
+  rw [NatIso.app_inv, NatIso.app_hom]
   apply NatIso.naturality_2
 #align category_theory.shift_zero' CategoryTheory.shiftZero'
 

diff --git a/Mathlib/Combinatorics/SimpleGraph/Coloring.lean b/Mathlib/Combinatorics/SimpleGraph/Coloring.lean
@@ -307,8 +307,8 @@ theorem colorable_chromaticNumber {m : ℕ} (hc : G.Colorable m) :
     G.Colorable (ENat.toNat G.chromaticNumber) := by
   classical
   rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]
-  apply Nat.find_spec
-  exact colorable_set_nonempty_of_colorable hc
+  · apply Nat.find_spec
+  · exact colorable_set_nonempty_of_colorable hc
 #align simple_graph.colorable_chromatic_number SimpleGraph.colorable_chromaticNumber
 
 theorem colorable_chromaticNumber_of_fintype (G : SimpleGraph V) [Finite V] :

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean
@@ -415,9 +415,17 @@ protected def equiv : CliffordAlgebra (0 : QuadraticForm R R) ≃ₐ[R] R[ε] :=
     (by
       ext : 1
       -- This used to be a single `simp` before leanprover/lean4#2644
-      simp; erw [lift_ι_apply]; simp)
+      simp only [QuadraticForm.zero_apply, AlgHom.coe_comp, Function.comp_apply, lift_apply_eps,
+        AlgHom.coe_id, id_eq]
+      erw [lift_ι_apply]
+      simp)
     -- This used to be a single `simp` before leanprover/lean4#2644
-    (by ext : 2; simp; erw [lift_ι_apply]; simp)
+    (by
+      ext : 2
+      simp only [QuadraticForm.zero_apply, AlgHom.comp_toLinearMap, LinearMap.coe_comp,
+        Function.comp_apply, AlgHom.toLinearMap_apply, AlgHom.toLinearMap_id, LinearMap.id_comp]
+      erw [lift_ι_apply]
+      simp)
 #align clifford_algebra_dual_number.equiv CliffordAlgebraDualNumber.equiv
 
 @[simp]

diff --git a/Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct/Basic.lean
@@ -761,8 +761,8 @@ Note that if `A` is commutative this can be instantiated with `S = A`.
 -/
 protected nonrec def rid : A ⊗[R] R ≃ₐ[S] A :=
   algEquivOfLinearEquivTensorProduct (AlgebraTensorModule.rid R S A)
-    (fun _a₁ _a₂ _r₁ _r₂ => smul_mul_smul _ _ _ _ |>.symm)
-    (one_smul _ _)
+    (fun a₁ a₂ r₁ r₂ => smul_mul_smul r₁ r₂ a₁ a₂ |>.symm)
+    (one_smul R _)
 #align algebra.tensor_product.rid Algebra.TensorProduct.rid
 
 @[simp] theorem rid_toLinearEquiv :