From 2134833ba690f9727f2b8bca170a995e0e9ce451 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 30 Apr 2024 04:53:13 +0000 Subject: [PATCH] chore: minor backports from nightly-testing (#12531) Co-authored-by: Scott Morrison --- Mathlib/CategoryTheory/Shift/Basic.lean | 2 ++ Mathlib/Combinatorics/SimpleGraph/Coloring.lean | 4 ++-- Mathlib/LinearAlgebra/CliffordAlgebra/Equivs.lean | 12 ++++++++++-- Mathlib/RingTheory/TensorProduct/Basic.lean | 4 ++-- 4 files changed, 16 insertions(+), 6 deletions(-) diff --git a/Mathlib/CategoryTheory/Shift/Basic.lean b/Mathlib/CategoryTheory/Shift/Basic.lean index 407cd6754097a1..121c50211dd51d 100644 --- 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 index 5841b9a2a34d5e..b0c19af0048b3d 100644 --- 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 index 8f936d174f5842..b2c812719b0ef0 100644 --- 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 index 2a7ca16b67fd6c..9aa6a9d7f7d668 100644 --- 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 :