[Merged by Bors] - chore: cleanup some simp-related porting notes

Mathlib/Algebra/Category/GroupCat/Injective.lean

@@ -156,4 +156,3 @@ instance injective_of_divisible [DivisibleBy A ℤ] :
 #align AddCommGroup.injective_of_divisible AddCommGroupCat.injective_of_divisible
 
 end AddCommGroupCat
-

Mathlib/Algebra/Category/ModuleCat/Colimits.lean

@@ -14,9 +14,9 @@ import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
 /-!
 # The category of R-modules has all colimits.
 
-This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`.
+This file uses a "pre-automated" approach, just as for `Mathlib.Algebra.Category.MonCat.Colimits`.
 
-Note that finite colimits can already be obtained from the instance `abelian (Module R)`.
+Note that finite colimits can already be obtained from the instance `Abelian (Module R)`.
 
 TODO:
 In fact, in `Module R` there is a much nicer model of colimits as quotients
@@ -362,8 +362,7 @@ def colimitCoconeIsColimit : IsColimit (colimitCocone F) where
       rfl
     · rw [quot_zero, map_zero] -- porting note: was `simp` but `map_zero` won't fire
       rfl
-    · rw [quot_neg, map_neg, map_neg, neg_inj] -- porting note: this was closed by `simp [*]`
-      assumption
+    · simpa
     · rw [quot_add, map_add, map_add]  -- porting note: this was closed by `simp [*]`
       congr 1
     · rw [quot_smul, map_smul, map_smul]  -- porting note: this was closed by `simp [*]`

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -922,49 +922,24 @@ theorem AddMonoidHom.apply_int [AddGroup M] (f : ℤ →+ M) (n : ℤ) : f n = n
 /-! `AddMonoidHom.ext_int` is defined in `Data.Int.Cast` -/
 
 variable (M G A)
--- Porting note: `simp` was broken during the port.
 /-- If `M` is commutative, `powersHom` is a multiplicative equivalence. -/
 def powersMulHom [CommMonoid M] : M ≃* (Multiplicative ℕ →* M) :=
-  { powersHom M with map_mul' := fun a b => MonoidHom.ext (by
-      intro n
-      let n' : ℕ := Multiplicative.toAdd n
-      show (a*b) ^ n' = a ^ n' * b ^ n'
-      simp [mul_pow]
-    ) }
+  { powersHom M with map_mul' := fun a b => MonoidHom.ext fun n => by simp [mul_pow] }
 #align powers_mul_hom powersMulHom
 
--- Porting note: `simp` was broken during the port.
 /-- If `M` is commutative, `zpowersHom` is a multiplicative equivalence. -/
 def zpowersMulHom [CommGroup G] : G ≃* (Multiplicative ℤ →* G) :=
-  { zpowersHom G with map_mul' := fun a b => MonoidHom.ext (by
-      intro n
-      let n' : ℤ := Multiplicative.toAdd n
-      show (a*b) ^ n' = a ^ n' * b ^ n'
-      simp [mul_zpow]
-    )
-  -- <| by simp [mul_zpow]
-  }
+  { zpowersHom G with map_mul' := fun a b => MonoidHom.ext fun n => by simp [mul_zpow] }
 #align zpowers_mul_hom zpowersMulHom
 
--- Porting note: `simp` was multiplesHom during the port.
 /-- If `M` is commutative, `multiplesHom` is an additive equivalence. -/
 def multiplesAddHom [AddCommMonoid A] : A ≃+ (ℕ →+ A) :=
-  { multiplesHom A with map_add' := fun a b => AddMonoidHom.ext (by
-      intro n
-      show n • (a+b) = n • a + n • b
-      simp [nsmul_add]
-  ) }
+  { multiplesHom A with map_add' := fun a b => AddMonoidHom.ext fun n => by simp [nsmul_add] }
 #align multiples_add_hom multiplesAddHom
 
 /-- If `M` is commutative, `zmultiplesHom` is an additive equivalence. -/
 def zmultiplesAddHom [AddCommGroup A] : A ≃+ (ℤ →+ A) :=
-  { zmultiplesHom A with map_add' := fun a b => AddMonoidHom.ext (by
-      intro n
-      show n • (a+b) = n • a + n • b
-      simp [zsmul_add]
-  )
-  -- <| by simp [zsmul_add]
-  }
+  { zmultiplesHom A with map_add' := fun a b => AddMonoidHom.ext fun n => by simp [zsmul_add] }
 #align zmultiples_add_hom zmultiplesAddHom
 
 variable {M G A}

Mathlib/Algebra/Hom/Ring.lean

@@ -578,21 +578,13 @@ protected theorem map_mul (f : α →+* β) : ∀ a b, f (a * b) = f a * f b :=
 @[simp]
 theorem map_ite_zero_one {F : Type _} [RingHomClass F α β] (f : F) (p : Prop) [Decidable p] :
     f (ite p 0 1) = ite p 0 1 := by
-  split_ifs with h
-  · simp only [h, ite_true]
-    rw [map_zero]
-  · simp only [h, ite_false]
-    rw [map_one] -- Porting note: `simp` is unable to apply `map_zero` or `map_one`!?
+  split_ifs with h <;> simp [h]
 #align ring_hom.map_ite_zero_one RingHom.map_ite_zero_one
 
 @[simp]
 theorem map_ite_one_zero {F : Type _} [RingHomClass F α β] (f : F) (p : Prop) [Decidable p] :
     f (ite p 1 0) = ite p 1 0 := by
-  split_ifs with h
-  · simp only [h, ite_true]
-    rw [map_one]
-  · simp only [h, ite_false]
-    rw [map_zero] -- Porting note: `simp` is unable to apply `map_zero` or `map_one`!?
+  split_ifs with h <;> simp [h]
 #align ring_hom.map_ite_one_zero RingHom.map_ite_one_zero
 
 /-- `f : α →+* β` has a trivial codomain iff `f 1 = 0`. -/
@@ -800,8 +792,7 @@ theorem coe_fn_mkRingHomOfMulSelfOfTwoNeZero (h h_two h_one) :
 -- @[simp]
 theorem coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero (h h_two h_one) :
     (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one : β →+ α) = f := by
-  apply AddMonoidHom.ext -- Porting note: why isn't `ext` picking up this lemma?
-  intro
+  ext
   rfl
 #align add_monoid_hom.coe_add_monoid_hom_mk_ring_hom_of_mul_self_of_two_ne_zero AddMonoidHom.coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero
 

Mathlib/Algebra/Homology/Augment.lean

@@ -345,8 +345,7 @@ def augmentTruncate (C : CochainComplex V ℕ) :
         rcases j with (_ | _ | j) <;> cases' i with i <;>
           · dsimp
             -- Porting note: simp can't handle this now but aesop does
-            aesop
-    }
+            aesop }
   hom_inv_id := by
     ext i
     cases i <;>
@@ -395,4 +394,3 @@ def fromSingle₀AsComplex [HasZeroObject V] (C : CochainComplex V ℕ) (X : V)
 #align cochain_complex.from_single₀_as_complex CochainComplex.fromSingle₀AsComplex
 
 end CochainComplex
-

Mathlib/Algebra/Lie/Nilpotent.lean

@@ -456,10 +456,7 @@ variable (hf : Surjective f) (hg : Surjective g) (hfg : ∀ x m, ⁅f x, g m⁆
 theorem Function.Surjective.lieModule_lcs_map_eq (k : ℕ) :
     (lowerCentralSeries R L M k : Submodule R M).map g = lowerCentralSeries R L₂ M₂ k := by
   induction' k with k ih
-  · -- Porting note: was `simp [LinearMap.range_eq_top, hg]`
-    simp only [Nat.zero_eq, lowerCentralSeries_zero, LieSubmodule.top_coeSubmodule,
-      Submodule.map_top, LinearMap.range_eq_top]
-    exact hg
+  · simpa [LinearMap.range_eq_top]
   · suffices
       g '' {m | ∃ (x : L) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} =
         {m | ∃ (x : L₂) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, g n⁆ = m} by

Mathlib/Algebra/Module/Submodule/Basic.lean

@@ -346,12 +346,10 @@ instance addCommMonoid : AddCommMonoid p :=
 instance module' [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] : Module S p :=
   { (show MulAction S p from p.toSubMulAction.mulAction') with
     smul := (· • ·)
-    -- Porting note: this used to be `ext <;> simp [add_smul, smul_add]` but `simp` tries
-    -- to prove it for the un-coerced version
-    smul_zero := fun a => Subtype.ext (smul_zero a)
-    zero_smul := fun a => Subtype.ext (zero_smul S (a : M))
-    add_smul := fun a b x => Subtype.ext (add_smul a b (x : M))
-    smul_add := fun a x y => Subtype.ext (smul_add a (x : M) (y : M)) }
+    smul_zero := fun a => by ext; simp
+    zero_smul := fun a => by ext; simp
+    add_smul := fun a b x => by ext; simp [add_smul]
+    smul_add := fun a x y => by ext; simp [smul_add] }
 #align submodule.module' Submodule.module'
 
 instance module : Module R p :=

Mathlib/Algebra/Module/ULift.lean

@@ -90,9 +90,7 @@ instance distribSmul [AddZeroClass M] [DistribSMul R M] : DistribSMul (ULift R)
 instance distribSmul' [AddZeroClass M] [DistribSMul R M] : DistribSMul R (ULift M) where
   smul_add c f g := by
     ext
-    -- Porting note: TODO this used to be a simple `simp [smul_add]` but that timeouts
-    simp only [smul_down, add_down]
-    rw [smul_add]
+    simp [smul_add]
 #align ulift.distrib_smul' ULift.distribSmul'
 
 instance distribMulAction [Monoid R] [AddMonoid M] [DistribMulAction R M] :
@@ -116,11 +114,9 @@ instance mulDistribMulAction' [Monoid R] [Monoid M] [MulDistribMulAction R M] :
   { ULift.mulAction' with
     smul_one := fun _ => by
       ext
-      dsimp only [smul_down, one_down]  -- Porting note: TODO this wasn't necessary
       simp [smul_one]
     smul_mul := fun _ _ _ => by
       ext
-      dsimp only [smul_down, mul_down] -- Porting note: TODO this wasn't necessary
       simp [smul_mul'] }
 #align ulift.mul_distrib_mul_action' ULift.mulDistribMulAction'
 

Mathlib/Algebra/Order/Group/Defs.lean

@@ -361,15 +361,13 @@ theorem mul_inv_le_inv_mul_iff : a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b :
 
 @[to_additive (attr := simp)]
 theorem div_le_self_iff (a : α) {b : α} : a / b ≤ a ↔ 1 ≤ b := by
-  -- Porting note: was `simp [div_eq_mul_inv]`
-  simp only [div_eq_mul_inv, mul_le_iff_le_one_right', Left.inv_le_one_iff]
+  simp [div_eq_mul_inv]
 #align div_le_self_iff div_le_self_iff
 #align sub_le_self_iff sub_le_self_iff
 
 @[to_additive (attr := simp)]
 theorem le_div_self_iff (a : α) {b : α} : a ≤ a / b ↔ b ≤ 1 := by
-  -- Porting note: was `simp [div_eq_mul_inv]`
-  simp only [div_eq_mul_inv, le_mul_iff_one_le_right', Left.one_le_inv_iff]
+  simp [div_eq_mul_inv]
 #align le_div_self_iff le_div_self_iff
 #align le_sub_self_iff le_sub_self_iff
 
@@ -421,8 +419,7 @@ theorem mul_inv_lt_inv_mul_iff : a * b⁻¹ < d⁻¹ * c ↔ d * a < c * b := by
 
 @[to_additive (attr := simp)]
 theorem div_lt_self_iff (a : α) {b : α} : a / b < a ↔ 1 < b := by
-  -- Porting note: was `simp [div_eq_mul_inv]`
-  simp only [div_eq_mul_inv, mul_lt_iff_lt_one_left', Left.inv_lt_one_iff]
+  simp [div_eq_mul_inv]
 #align div_lt_self_iff div_lt_self_iff
 #align sub_lt_self_iff sub_lt_self_iff
 

Mathlib/Algebra/Order/Ring/WithTop.lean

@@ -151,7 +151,8 @@ protected def _root_.MonoidWithZeroHom.withTopMap {R S : Type _} [MulZeroOneClas
       induction' y using WithTop.recTopCoe with y
       · have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
         simp [mul_top hx, mul_top this]
-      · simp only [map_coe, ← coe_mul, map_mul] } -- porting note: todo: `simp [← coe_mul]` fails
+      · -- porting note: todo: `simp [← coe_mul]` times out
+        simp only [map_coe, ← coe_mul, map_mul] }
 #align monoid_with_zero_hom.with_top_map MonoidWithZeroHom.withTopMap
 
 instance [SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithTop α) :=

Mathlib/Algebra/Star/Module.lean

@@ -182,11 +182,7 @@ def StarModule.decomposeProdAdjoint : A ≃ₗ[R] selfAdjoint A × skewAdjoint A
   refine LinearEquiv.ofLinear ((selfAdjointPart R).prod (skewAdjointPart R))
     (LinearMap.coprod ((selfAdjoint.submodule R A).subtype) (skewAdjoint.submodule R A).subtype)
     ?_ (LinearMap.ext <| StarModule.selfAdjointPart_add_skewAdjointPart R)
-  -- Porting note: The remaining proof at this point used to be `ext <;> simp`.
-  simp only [LinearMap.comp_coprod, LinearMap.prod_comp, selfAdjointPart_comp_subtype_selfAdjoint,
-    selfAdjointPart_comp_subtype_skewAdjoint, skewAdjointPart_comp_subtype_selfAdjoint,
-    skewAdjointPart_comp_subtype_skewAdjoint, LinearMap.coprod_zero_left,
-    LinearMap.coprod_zero_right, LinearMap.id_comp, LinearMap.pair_fst_snd]
+  ext <;> simp
 #align star_module.decompose_prod_adjoint StarModule.decomposeProdAdjoint
 
 @[simp]