chore: address and delete many porting notes across the library (#19685)

j-loreaux · j-loreaux · commit 64f356003c7a · 2024-12-10T02:59:32.000Z
diff --git a/Archive/Imo/Imo1972Q5.lean b/Archive/Imo/Imo1972Q5.lean
@@ -80,11 +80,10 @@ This is a more concise version of the proof proposed by Ruben Van de Velde.
 -/
 theorem imo1972_q5' (f g : ℝ → ℝ) (hf1 : ∀ x, ∀ y, f (x + y) + f (x - y) = 2 * f x * g y)
     (hf2 : BddAbove (Set.range fun x => ‖f x‖)) (hf3 : ∃ x, f x ≠ 0) (y : ℝ) : ‖g y‖ ≤ 1 := by
-  -- Porting note: moved `by_contra!` up to avoid a bug
-  by_contra! H
   obtain ⟨x, hx⟩ := hf3
   set k := ⨆ x, ‖f x‖
   have h : ∀ x, ‖f x‖ ≤ k := le_ciSup hf2
+  by_contra! H
   have hgy : 0 < ‖g y‖ := by linarith
   have k_pos : 0 < k := lt_of_lt_of_le (norm_pos_iff.mpr hx) (h x)
   have : k / ‖g y‖ < k := (div_lt_iff₀ hgy).mpr (lt_mul_of_one_lt_right k_pos H)
diff --git a/Archive/Imo/Imo2013Q1.lean b/Archive/Imo/Imo2013Q1.lean
@@ -27,7 +27,6 @@ We prove a slightly more general version where k does not need to be strictly po
 
 namespace Imo2013Q1
 
--- Porting note: simplified proof using `positivity`
 theorem arith_lemma (k n : ℕ) : 0 < 2 * n + 2 ^ k.succ := by positivity
 
 theorem prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) :
diff --git a/Archive/MiuLanguage/DecisionNec.lean b/Archive/MiuLanguage/DecisionNec.lean
@@ -154,9 +154,7 @@ theorem goodm_of_rule3 (as bs : Miustr) (h₁ : Derivable (as ++ ↑[I, I, I] ++
     exact mhead
   · contrapose! nmtail
     rcases exists_cons_of_ne_nil k with ⟨x, xs, rfl⟩
-    -- Porting note: `simp_rw [cons_append]` didn't work
-    rw [cons_append] at nmtail; rw [cons_append, cons_append]
-    dsimp only [tail] at nmtail ⊢
+    simp_rw [cons_append] at nmtail ⊢
     simpa using nmtail
 
 /-!
@@ -174,9 +172,7 @@ theorem goodm_of_rule4 (as bs : Miustr) (h₁ : Derivable (as ++ ↑[U, U] ++ bs
     exact mhead
   · contrapose! nmtail
     rcases exists_cons_of_ne_nil k with ⟨x, xs, rfl⟩
-    -- Porting note: `simp_rw [cons_append]` didn't work
-    rw [cons_append] at nmtail; rw [cons_append, cons_append]
-    dsimp only [tail] at nmtail ⊢
+    simp_rw [cons_append] at nmtail ⊢
     simpa using nmtail
 
 /-- Any derivable string must begin with `M` and have no `M` in its tail.
diff --git a/Archive/MiuLanguage/DecisionSuf.lean b/Archive/MiuLanguage/DecisionSuf.lean
@@ -308,10 +308,8 @@ theorem ind_hyp_suf (k : ℕ) (ys : Miustr) (hu : count U ys = succ k) (hdec : D
   rcases eq_append_cons_U_of_count_U_pos hu with ⟨as, bs, rfl⟩
   use as, bs
   refine ⟨rfl, ?_, ?_, ?_⟩
-  · -- Porting note: `simp_rw [count_append]` didn't work
-    rw [count_append] at hu
-    simp_rw [count_cons, beq_self_eq_true, if_true, add_succ, beq_iff_eq, reduceCtorEq, reduceIte,
-      add_zero, succ_inj'] at hu
+  · simp_rw [count_append, count_cons, beq_self_eq_true, if_true, add_succ, beq_iff_eq,
+      reduceCtorEq, reduceIte, add_zero, succ_inj'] at hu
     rwa [count_append, count_append]
   · apply And.intro rfl
     rw [cons_append, cons_append]
diff --git a/Mathlib/Algebra/AddTorsor.lean b/Mathlib/Algebra/AddTorsor.lean
@@ -87,7 +87,6 @@ theorem vadd_vsub (g : G) (p : P) : (g +ᵥ p) -ᵥ p = g :=
 /-- If the same point added to two group elements produces equal
 results, those group elements are equal. -/
 theorem vadd_right_cancel {g₁ g₂ : G} (p : P) (h : g₁ +ᵥ p = g₂ +ᵥ p) : g₁ = g₂ := by
--- Porting note: vadd_vsub g₁ → vadd_vsub g₁ p
   rw [← vadd_vsub g₁ p, h, vadd_vsub]
 
 @[simp]
@@ -364,8 +363,6 @@ def constVAddHom : Multiplicative G →* Equiv.Perm P where
 
 variable {P}
 
--- Porting note: Previous code was:
--- open _Root_.Function
 open Function
 
 /-- Point reflection in `x` as a permutation. -/
@@ -412,7 +409,6 @@ theorem pointReflection_fixed_iff_of_injective_two_nsmul {x y : P} (h : Injectiv
 @[deprecated (since := "2024-11-18")] alias pointReflection_fixed_iff_of_injective_bit0 :=
 pointReflection_fixed_iff_of_injective_two_nsmul
 
--- Porting note: need this to calm down CI
 theorem injective_pointReflection_left_of_injective_two_nsmul {G P : Type*} [AddCommGroup G]
     [AddTorsor G P] (h : Injective (2 • · : G → G)) (y : P) :
     Injective fun x : P => pointReflection x y :=
diff --git a/Mathlib/Algebra/BigOperators/Finsupp.lean b/Mathlib/Algebra/BigOperators/Finsupp.lean
@@ -242,12 +242,10 @@ theorem sum_apply [Zero M] [AddCommMonoid N] {f : α →₀ M} {g : α → M →
     (f.sum g) a₂ = f.sum fun a₁ b => g a₁ b a₂ :=
   finset_sum_apply _ _ _
 
--- Porting note: inserted ⇑ on the rhs
 @[simp, norm_cast] theorem coe_finset_sum [AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) :
     ⇑(∑ i ∈ S, f i) = ∑ i ∈ S, ⇑(f i) :=
   map_sum (coeFnAddHom : (α →₀ N) →+ _) _ _
 
--- Porting note: inserted ⇑ on the rhs
 @[simp, norm_cast] theorem coe_sum [Zero M] [AddCommMonoid N] (f : α →₀ M) (g : α → M → β →₀ N) :
     ⇑(f.sum g) = f.sum fun a₁ b => ⇑(g a₁ b) :=
   coe_finset_sum _ _
@@ -381,14 +379,12 @@ theorem univ_sum_single [Fintype α] [AddCommMonoid M] (f : α →₀ M) :
 @[simp]
 theorem univ_sum_single_apply [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
     ∑ j : α, single i m j = m := by
-  -- Porting note: rewrite due to leaky classical in lean3
   classical rw [single, coe_mk, Finset.sum_pi_single']
   simp
 
 @[simp]
 theorem univ_sum_single_apply' [AddCommMonoid M] [Fintype α] (i : α) (m : M) :
     ∑ j : α, single j m i = m := by
-  -- Porting note: rewrite due to leaky classical in lean3
   simp_rw [single, coe_mk]
   classical rw [Finset.sum_pi_single]
   simp
@@ -454,7 +450,6 @@ theorem support_sum_eq_biUnion {α : Type*} {ι : Type*} {M : Type*} [DecidableE
     (h : ∀ i₁ i₂, i₁ ≠ i₂ → Disjoint (g i₁).support (g i₂).support) :
     (∑ i ∈ s, g i).support = s.biUnion fun i => (g i).support := by
   classical
-  -- Porting note: apply Finset.induction_on s was not working; refine does.
   refine Finset.induction_on s ?_ ?_
   · simp
   · intro i s hi
@@ -578,7 +573,6 @@ end
 
 namespace Nat
 
--- Porting note: Needed to replace pow with (· ^ ·)
 /-- If `0 : ℕ` is not in the support of `f : ℕ →₀ ℕ` then `0 < ∏ x ∈ f.support, x ^ (f x)`. -/
 theorem prod_pow_pos_of_zero_not_mem_support {f : ℕ →₀ ℕ} (nhf : 0 ∉ f.support) :
     0 < f.prod (· ^ ·) :=
diff --git a/Mathlib/Algebra/BigOperators/Group/Finset.lean b/Mathlib/Algebra/BigOperators/Group/Finset.lean
@@ -1216,8 +1216,7 @@ lemma prod_mulIndicator_subset_of_eq_one [One α] (f : ι → α) (g : ι → α
     ∏ i ∈ t, g i (mulIndicator ↑s f i) = ∏ i ∈ s, g i (f i) := by
   calc
     _ = ∏ i ∈ s, g i (mulIndicator ↑s f i) := by rw [prod_subset h fun i _ hn ↦ by simp [hn, hg]]
-    -- Porting note: This did not use to need the implicit argument
-    _ = _ := prod_congr rfl fun i hi ↦ congr_arg _ <| mulIndicator_of_mem (α := ι) hi f
+    _ = _ := prod_congr rfl fun i hi ↦ congr_arg _ <| mulIndicator_of_mem hi f
 
 /-- Taking the product of an indicator function over a possibly larger finset is the same as
 taking the original function over the original finset. -/
diff --git a/Mathlib/Algebra/BigOperators/Group/Multiset.lean b/Mathlib/Algebra/BigOperators/Group/Multiset.lean
@@ -187,7 +187,6 @@ theorem prod_induction (p : α → Prop) (s : Multiset α) (p_mul : ∀ a b, p a
 @[to_additive]
 theorem prod_induction_nonempty (p : α → Prop) (p_mul : ∀ a b, p a → p b → p (a * b)) (hs : s ≠ ∅)
     (p_s : ∀ a ∈ s, p a) : p s.prod := by
-  -- Porting note: used to be `refine' Multiset.induction _ _`
   induction s using Multiset.induction_on with
   | empty => simp at hs
   | cons a s hsa =>
@@ -263,8 +262,7 @@ theorem prod_map_inv' (m : Multiset α) : (m.map Inv.inv).prod = m.prod⁻¹ :=
 
 @[to_additive (attr := simp)]
 theorem prod_map_inv : (m.map fun i => (f i)⁻¹).prod = (m.map f).prod⁻¹ := by
-  -- Porting note: used `convert`
-  simp_rw [← (m.map f).prod_map_inv', map_map, Function.comp_apply]
+  rw [← (m.map f).prod_map_inv', map_map, Function.comp_def]
 
 @[to_additive (attr := simp)]
 theorem prod_map_div : (m.map fun i => f i / g i).prod = (m.map f).prod / (m.map g).prod :=
diff --git a/Mathlib/Algebra/Category/Grp/Colimits.lean b/Mathlib/Algebra/Category/Grp/Colimits.lean
@@ -209,8 +209,7 @@ def descFun (s : Cocone F) : ColimitType.{w} F → s.pt := by
 def descMorphism (s : Cocone F) : colimit.{w} F ⟶ s.pt where
   toFun := descFun F s
   map_zero' := rfl
-  -- Porting note: in `mathlib3`, nothing needs to be done after `induction`
-  map_add' x y := Quot.induction_on₂ x y fun _ _ => by dsimp; rw [← quot_add F]; rfl
+  map_add' x y := Quot.induction_on₂ x y fun _ _ ↦ rfl
 
 /-- Evidence that the proposed colimit is the colimit. -/
 def colimitCoconeIsColimit : IsColimit (colimitCocone.{w} F) where
diff --git a/Mathlib/Algebra/Category/Grp/EquivalenceGroupAddGroup.lean b/Mathlib/Algebra/Category/Grp/EquivalenceGroupAddGroup.lean
@@ -20,12 +20,6 @@ open CategoryTheory
 
 namespace Grp
 
--- Porting note: Lean cannot find these now
-private instance (X : Grp) : MulOneClass X.α := X.str.toMulOneClass
-private instance (X : CommGrp) : MulOneClass X.α := X.str.toMulOneClass
-private instance (X : AddGrp) : AddZeroClass X.α := X.str.toAddZeroClass
-private instance (X : AddCommGrp) : AddZeroClass X.α := X.str.toAddZeroClass
-
 /-- The functor `Grp ⥤ AddGrp` by sending `X ↦ Additive X` and `f ↦ f`.
 -/
 @[simps]
diff --git a/Mathlib/Algebra/CubicDiscriminant.lean b/Mathlib/Algebra/CubicDiscriminant.lean
@@ -468,12 +468,8 @@ def disc {R : Type*} [Ring R] (P : Cubic R) : R :=
 
 theorem disc_eq_prod_three_roots (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
     φ P.disc = (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2 := by
-  simp only [disc, RingHom.map_add, RingHom.map_sub, RingHom.map_mul, map_pow]
-  -- Porting note: Replaced `simp only [RingHom.map_one, map_bit0, map_bit1]` with f4, f18, f27
-  have f4 : φ 4 = 4 := map_natCast φ 4
-  have f18 : φ 18 = 18 := map_natCast φ 18
-  have f27 : φ 27 = 27 := map_natCast φ 27
-  rw [f4, f18, f27, b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]
+  simp only [disc, RingHom.map_add, RingHom.map_sub, RingHom.map_mul, map_pow, map_ofNat]
+  rw [b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]
   ring1
 
 theorem disc_ne_zero_iff_roots_ne (ha : P.a ≠ 0) (h3 : (map φ P).roots = {x, y, z}) :
diff --git a/Mathlib/Algebra/DirectLimit.lean b/Mathlib/Algebra/DirectLimit.lean
@@ -315,11 +315,7 @@ theorem of.zero_exact [IsDirected ι (· ≤ ·)] {i x} (H : of R ι G f i x = 0
   if hx0 : x = 0 then ⟨i, le_rfl, by simp [hx0]⟩
   else
     have hij : i ≤ j := hj _ <| by simp [DirectSum.apply_eq_component, hx0]
-    ⟨j, hij, by
-      -- Porting note: this had been
-      -- simpa [totalize_of_le hij] using hxj
-      simp only [DirectSum.toModule_lof] at hxj
-      rwa [totalize_of_le hij] at hxj⟩
+    ⟨j, hij, by simpa [totalize, dif_pos hij, totalize_of_le hij] using hxj⟩
 
 end DirectLimit
 
@@ -731,8 +727,7 @@ theorem of.zero_exact_aux [Nonempty ι] [IsDirected ι (· ≤ ·)] {x : FreeCom
       ⟨k, ↑s ∪ t, this,
         isSupported_mul (isSupported_upwards hxs Set.subset_union_left)
           (isSupported_upwards hyt Set.subset_union_right), fun [_] => ?_⟩
-    -- Porting note: RingHom.map_mul was `(restriction _).map_mul`
-    classical rw [RingHom.map_mul, (FreeCommRing.lift _).map_mul, ←
+    classical rw [(restriction _).map_mul, (FreeCommRing.lift _).map_mul, ←
       of.zero_exact_aux2 G f' hyt hj this hjk Set.subset_union_right, iht,
       (f' j k hjk).map_zero, mul_zero]
 
diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean
@@ -346,7 +346,6 @@ protected theorem Commute.geom_sum₂_Ico_mul [Ring α] {x y : α} (h : Commute
     have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
     simpa [Commute, SemiconjBy] using hp
   simp only [this]
-  -- Porting note: gives deterministic timeout without this intermediate `have`
   convert (Commute.op h).mul_geom_sum₂_Ico hmn
 
 theorem geom_sum_Ico_mul [Ring α] (x : α) {m n : ℕ} (hmn : m ≤ n) :
diff --git a/Mathlib/Algebra/Lie/Submodule.lean b/Mathlib/Algebra/Lie/Submodule.lean
@@ -1209,15 +1209,9 @@ lemma incl_injective (I : LieIdeal R L) : Function.Injective I.incl :=
 
 @[simp]
 theorem comap_incl_self : comap I.incl I = ⊤ := by ext; simp
-  --  porting note: `ext; simp` works also in mathlib3, though the proof used to be
-  --  rw [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.top_coeSubmodule,
-  --    LieIdeal.comap_coeSubmodule, LieIdeal.incl_coe, Submodule.comap_subtype_self]
 
 @[simp]
 theorem ker_incl : I.incl.ker = ⊥ := by ext; simp
-  --  porting note: `ext; simp` works also in mathlib3, though the proof used to be
-  --  rw [← LieSubmodule.coe_toSubmodule_eq_iff, I.incl.ker_coeSubmodule,
-  --    LieSubmodule.bot_coeSubmodule, incl_coe, Submodule.ker_subtype]
 
 @[simp]
 theorem incl_idealRange : I.incl.idealRange = I := by
diff --git a/Mathlib/Algebra/Quandle.lean b/Mathlib/Algebra/Quandle.lean
@@ -417,7 +417,6 @@ def Conj.map {G : Type*} {H : Type*} [Group G] [Group H] (f : G →* H) : Conj G
 
 Used for Fox n-colorings of knots.
 -/
--- Porting note: Removed nolint
 def Dihedral (n : ℕ) :=
   ZMod n
 
diff --git a/Mathlib/Algebra/Quaternion.lean b/Mathlib/Algebra/Quaternion.lean
@@ -148,7 +148,7 @@ theorem coe_injective : Function.Injective (coe : R → ℍ[R,c₁,c₂]) := fun
 theorem coe_inj {x y : R} : (x : ℍ[R,c₁,c₂]) = y ↔ x = y :=
   coe_injective.eq_iff
 
--- Porting note: removed `simps`, added simp lemmas manually
+-- Porting note: removed `simps`, added simp lemmas manually. Should adjust `simps` to name properly
 instance : Zero ℍ[R,c₁,c₂] := ⟨⟨0, 0, 0, 0⟩⟩
 
 @[simp] theorem zero_re : (0 : ℍ[R,c₁,c₂]).re = 0 := rfl
@@ -169,7 +169,7 @@ instance : Inhabited ℍ[R,c₁,c₂] := ⟨0⟩
 section One
 variable [One R]
 
--- Porting note: removed `simps`, added simp lemmas manually
+-- Porting note: removed `simps`, added simp lemmas manually. Should adjust `simps` to name properly
 instance : One ℍ[R,c₁,c₂] := ⟨⟨1, 0, 0, 0⟩⟩
 
 @[simp] theorem one_re : (1 : ℍ[R,c₁,c₂]).re = 1 := rfl
@@ -190,7 +190,7 @@ end Zero
 section Add
 variable [Add R]
 
--- Porting note: removed `simps`, added simp lemmas manually
+-- Porting note: removed `simps`, added simp lemmas manually. Should adjust `simps` to name properly
 instance : Add ℍ[R,c₁,c₂] :=
   ⟨fun a b => ⟨a.1 + b.1, a.2 + b.2, a.3 + b.3, a.4 + b.4⟩⟩
 
@@ -223,7 +223,7 @@ end AddZeroClass
 section Neg
 variable [Neg R]
 
--- Porting note: removed `simps`, added simp lemmas manually
+-- Porting note: removed `simps`, added simp lemmas manually. Should adjust `simps` to name properly
 instance : Neg ℍ[R,c₁,c₂] := ⟨fun a => ⟨-a.1, -a.2, -a.3, -a.4⟩⟩
 
 @[simp] theorem neg_re : (-a).re = -a.re := rfl
@@ -718,6 +718,7 @@ end QuaternionAlgebra
 def Quaternion (R : Type*) [One R] [Neg R] :=
   QuaternionAlgebra R (-1) (-1)
 
+@[inherit_doc]
 scoped[Quaternion] notation "ℍ[" R "]" => Quaternion R
 
 /-- The equivalence between the quaternions over `R` and `R × R × R × R`. -/
@@ -1224,8 +1225,6 @@ instance instGroupWithZero : GroupWithZero ℍ[R] :=
     inv := Inv.inv
     inv_zero := by rw [instInv_inv, star_zero, smul_zero]
     mul_inv_cancel := fun a ha => by
-      -- Porting note: the aliased definition confuse TC search
-      letI : Semiring ℍ[R] := inferInstanceAs (Semiring ℍ[R,-1,-1])
       rw [instInv_inv, Algebra.mul_smul_comm (normSq a)⁻¹ a (star a), self_mul_star, smul_coe,
         inv_mul_cancel₀ (normSq_ne_zero.2 ha), coe_one] }
 
diff --git a/Mathlib/Analysis/Normed/Lp/LpEquiv.lean b/Mathlib/Analysis/Normed/Lp/LpEquiv.lean
@@ -91,9 +91,6 @@ section Equivₗᵢ
 
 variable [Fintype α] (𝕜 : Type*) [NontriviallyNormedField 𝕜] [∀ i, NormedSpace 𝕜 (E i)]
 variable (E)
-/- porting note: Lean is unable to work with `lpPiLpₗᵢ` if `E` is implicit without
-annotating with `(E := E)` everywhere, so we just make it explicit. This file has no
-dependencies. -/
 
 /-- The canonical `LinearIsometryEquiv` between `lp E p` and `PiLp p E` when `E : α → Type u`
 with `[Fintype α]` and `[Fact (1 ≤ p)]`. -/
@@ -145,9 +142,6 @@ theorem coe_addEquiv_lpBCF_symm (f : α →ᵇ E) : (AddEquiv.lpBCF.symm f : α
   rfl
 
 variable (E)
-/- porting note: Lean is unable to work with `lpPiLpₗᵢ` if `E` is implicit without
-annotating with `(E := E)` everywhere, so we just make it explicit. This file has no
-dependencies. -/
 
 /-- The canonical map between `lp (fun _ : α ↦ E) ∞` and `α →ᵇ E` as a `LinearIsometryEquiv`. -/
 noncomputable def lpBCFₗᵢ : lp (fun _ : α ↦ E) ∞ ≃ₗᵢ[𝕜] α →ᵇ E :=
diff --git a/Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean b/Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean
@@ -76,10 +76,6 @@ def mkOfHomPrefunctors (F : B → C) (F' : (a : B) → (b : B) → Prefunctor (a
   map {a b} := (F' a b).obj
   map₂ {a b} := (F' a b).map
 
--- Porting note: deleted syntactic tautologies `toPrefunctor_eq_coe : F.toPrefunctor = F`
--- and `to_prefunctor_obj : (F : Prefunctor B C).obj = F.obj`
--- and `to_prefunctor_map`
-
 /-- The identity lax prefunctor. -/
 @[simps]
 def id (B : Type u₁) [Quiver.{v₁ + 1} B] [∀ a b : B, Quiver.{w₁ + 1} (a ⟶ b)] :
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -992,11 +992,10 @@ end
 
 variable {G : J ⥤ C} (α : F ⟶ G)
 
--- @[reassoc (attr := simp)] Porting note: now simp can prove these
 @[reassoc]
 theorem colimit.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫ colimit.ι G j := by simp
 
-@[simp] -- Porting note: proof adjusted to account for @[simps] on all fields of colim
+@[simp]
 theorem colimit.map_desc (c : Cocone G) :
     colimMap α ≫ colimit.desc G c = colimit.desc F ((Cocones.precompose α).obj c) := by
   ext j
@@ -1125,8 +1124,7 @@ def IsColimit.op {t : Cocone F} (P : IsColimit t) : IsLimit t.op where
 -/
 def IsLimit.unop {t : Cone F.op} (P : IsLimit t) : IsColimit t.unop where
   desc s := (P.lift s.op).unop
-  fac s j := congrArg Quiver.Hom.unop (P.fac s.op (Opposite.op j))
-  -- Porting note: thinks `op j` is `IsLimit.op j`
+  fac s j := congrArg Quiver.Hom.unop (P.fac s.op (.op j))
   uniq s m w := by
     dsimp
     rw [← P.uniq s.op m.op]
@@ -1140,8 +1138,7 @@ def IsLimit.unop {t : Cone F.op} (P : IsLimit t) : IsColimit t.unop where
 -/
 def IsColimit.unop {t : Cocone F.op} (P : IsColimit t) : IsLimit t.unop where
   lift s := (P.desc s.op).unop
-  fac s j := congrArg Quiver.Hom.unop (P.fac s.op (Opposite.op j))
-  -- Porting note: thinks `op j` is `IsLimit.op j`
+  fac s j := congrArg Quiver.Hom.unop (P.fac s.op (.op j))
   uniq s m w := by
     dsimp
     rw [← P.uniq s.op m.op]
diff --git a/Mathlib/Data/List/DropRight.lean b/Mathlib/Data/List/DropRight.lean
@@ -138,18 +138,9 @@ theorem dropWhile_eq_self_iff : dropWhile p l = l ↔ ∀ hl : 0 < l.length, ¬p
       rw [get] at this
       simp_rw [this]
 
-/- porting note: This proof is longer than it used to be because `simp` refuses to rewrite
- the `l ≠ []` condition if `hl` is not `intro`'d yet -/
 @[simp]
 theorem rdropWhile_eq_self_iff : rdropWhile p l = l ↔ ∀ hl : l ≠ [], ¬p (l.getLast hl) := by
-  simp only [rdropWhile, reverse_eq_iff, dropWhile_eq_self_iff, getLast_eq_getElem]
-  refine ⟨fun h hl => ?_, fun h hl => ?_⟩
-  · rw [← length_pos, ← length_reverse] at hl
-    have := h hl
-    rwa [get_reverse'] at this
-  · rw [length_reverse, length_pos] at hl
-    have := h hl
-    rwa [get_reverse']
+  simp [rdropWhile, reverse_eq_iff, getLast_eq_getElem, Nat.pos_iff_ne_zero]
 
 variable (p) (l)
 
diff --git a/Mathlib/Data/Set/Basic.lean b/Mathlib/Data/Set/Basic.lean
@@ -1007,7 +1007,6 @@ def subtypeInsertEquivOption
 
 /-! ### Lemmas about singletons -/
 
-/- porting note: instance was in core in Lean3 -/
 instance : LawfulSingleton α (Set α) :=
   ⟨fun x => Set.ext fun a => by
     simp only [mem_empty_iff_false, mem_insert_iff, or_false]
diff --git a/Mathlib/GroupTheory/GroupAction/Hom.lean b/Mathlib/GroupTheory/GroupAction/Hom.lean
diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
diff --git a/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
diff --git a/Mathlib/RingTheory/WittVector/IsPoly.lean b/Mathlib/RingTheory/WittVector/IsPoly.lean
diff --git a/Mathlib/Topology/Gluing.lean b/Mathlib/Topology/Gluing.lean
diff --git a/Mathlib/Topology/UniformSpace/Completion.lean b/Mathlib/Topology/UniformSpace/Completion.lean
