chore: minor cleanup after eta's return (#4028)

leanprover-community · May 16, 2023 · f44ff70 · f44ff70
1 parent 95a9188
commit f44ff70
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 8 deletions.
diff --git a/Mathlib/Algebra/Star/Subalgebra.lean b/Mathlib/Algebra/Star/Subalgebra.lean
@@ -60,9 +60,6 @@ instance subsemiringClass : SubsemiringClass (StarSubalgebra R A) A where
   one_mem {s} := s.one_mem'
   zero_mem {s} := s.zero_mem'
 
--- porting note: work around lean4#2074
-attribute [-instance] Ring.toNonAssocRing Ring.toNonUnitalRing CommRing.toNonUnitalCommRing
-
 instance subringClass {R A} [CommRing R] [StarRing R] [Ring A] [StarRing A] [Algebra R A]
     [StarModule R A] : SubringClass (StarSubalgebra R A) A where
   neg_mem {s a} ha := show -a ∈ s.toSubalgebra from neg_mem ha
@@ -571,9 +568,6 @@ def adjoinCommSemiringOfComm {s : Set A} (hcomm : ∀ a : A, a ∈ s → ∀ b :
       exact congr_arg Subtype.val (mul_comm (⟨x, hx⟩ : Algebra.adjoin R (s ∪ star s)) ⟨y, hy⟩) }
 #align star_subalgebra.adjoin_comm_semiring_of_comm StarSubalgebra.adjoinCommSemiringOfComm
 
--- porting note: work around lean4#2074
-attribute [-instance] Ring.toNonAssocRing Ring.toNonUnitalRing CommRing.toNonUnitalCommRing
-
 /-- If all elements of `s : Set A` commute pairwise and also commute pairwise with elements of
 `star s`, then `StarSubalgebra.adjoin R s` is commutative. See note [reducible non-instances]. -/
 @[reducible]

diff --git a/Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean b/Mathlib/LinearAlgebra/FreeModule/Finite/Rank.lean
@@ -101,7 +101,7 @@ theorem finrank_finsupp {ι : Type v} [Fintype ι] : finrank R (ι →₀ R) = c
 
 /-- The finrank of `(ι → R)` is `Fintype.card ι`. -/
 theorem finrank_pi {ι : Type v} [Fintype ι] : finrank R (ι → R) = card ι := by
-    simp [finrank]
+  simp [finrank]
 #align finite_dimensional.finrank_pi FiniteDimensional.finrank_pi
 
 /-- The finrank of the direct sum is the sum of the finranks. -/

diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant.lean b/Mathlib/LinearAlgebra/Matrix/Determinant.lean
@@ -150,7 +150,7 @@ theorem det_mul_aux {M N : Matrix n n R} {p : n → n} (H : ¬Bijective p) :
       mul_swap_involutive i j σ
 #align matrix.det_mul_aux Matrix.det_mul_aux
 
--- Porting note: need to bump for last simp
+-- Porting note: need to bump for last simp; new after #3414 (reenableeta)
 set_option maxHeartbeats 300000 in
 @[simp]
 theorem det_mul (M N : Matrix n n R) : det (M ⬝ N) = det M * det N :=