chore: clear some porting notes on rfl (#8063)

We remove some porting notes for `rfl`s that by now work again.




Co-authored-by: Moritz Firsching <[email protected]>

Mathlib/Algebra/DirectLimit.lean

@@ -128,8 +128,7 @@ theorem exists_of [Nonempty ι] [IsDirected ι (· ≤ ·)] (z : DirectLimit G f
         let ⟨k, hik, hjk⟩ := exists_ge_ge i j
         ⟨k, f i k hik x + f j k hjk y, by
           rw [LinearMap.map_add, of_f, of_f, ihx, ihy]
-          -- porting note: was `rfl`
-          simp only [Submodule.Quotient.mk''_eq_mk, Quotient.mk_add]⟩
+          rfl ⟩
 #align module.direct_limit.exists_of Module.DirectLimit.exists_of
 
 @[elab_as_elim]

Mathlib/Algebra/Lie/Submodule.lean

@@ -320,8 +320,7 @@ theorem exists_lieIdeal_coe_eq_iff :
     (∃ I : LieIdeal R L, ↑I = K) ↔ ∀ x y : L, y ∈ K → ⁅x, y⁆ ∈ K := by
   simp only [← coe_to_submodule_eq_iff, LieIdeal.coe_to_lieSubalgebra_to_submodule,
     Submodule.exists_lieSubmodule_coe_eq_iff L]
-  -- Porting note: was `exact Iff.rfl`
-  simp only [mem_coe_submodule]
+  exact Iff.rfl
 #align lie_subalgebra.exists_lie_ideal_coe_eq_iff LieSubalgebra.exists_lieIdeal_coe_eq_iff
 
 theorem exists_nested_lieIdeal_coe_eq_iff {K' : LieSubalgebra R L} (h : K ≤ K') :

Mathlib/Algebra/Order/Ring/Defs.lean

@@ -800,12 +800,9 @@ theorem nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg (hab : 0 ≤ a * b)
     0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0 := by
   refine' Decidable.or_iff_not_and_not.2 _
   simp only [not_and, not_le]; intro ab nab; apply not_lt_of_le hab _
-  -- Porting note: for the middle case, we used to have `rfl`, but it is now rejected.
-  -- https://github.com/leanprover/std4/issues/62
-  rcases lt_trichotomy 0 a with (ha | ha | ha)
+  rcases lt_trichotomy 0 a with (ha | rfl | ha)
   · exact mul_neg_of_pos_of_neg ha (ab ha.le)
-  · subst ha
-    exact ((ab le_rfl).asymm (nab le_rfl)).elim
+  · exact ((ab le_rfl).asymm (nab le_rfl)).elim
   · exact mul_neg_of_neg_of_pos ha (nab ha.le)
 #align nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nnonneg nonneg_and_nonneg_or_nonpos_and_nonpos_of_mul_nonneg
 
@@ -835,11 +832,8 @@ theorem nonpos_of_mul_nonpos_right (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0 :=
 
 @[simp]
 theorem zero_le_mul_left (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b := by
-  -- Porting note: this used to be by:
-  -- convert mul_le_mul_left h
-  -- simp
-  -- but the `convert` no longer works.
-  simpa using (mul_le_mul_left h : c * 0 ≤ c * b ↔ 0 ≤ b)
+  convert mul_le_mul_left h
+  simp
 #align zero_le_mul_left zero_le_mul_left
 
 @[simp]

Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean

@@ -67,8 +67,8 @@ theorem incMatrix_apply [Zero R] [One R] {a : α} {e : Sym2 α} :
 /-- Entries of the incidence matrix can be computed given additional decidable instances. -/
 theorem incMatrix_apply' [Zero R] [One R] [DecidableEq α] [DecidableRel G.Adj] {a : α}
     {e : Sym2 α} : G.incMatrix R a e = if e ∈ G.incidenceSet a then 1 else 0 := by
-  unfold incMatrix Set.indicator -- Porting note: was `convert rfl`
-  simp only [Pi.one_apply]
+  unfold incMatrix Set.indicator
+  convert rfl
 #align simple_graph.inc_matrix_apply' SimpleGraph.incMatrix_apply'
 
 section MulZeroOneClass

Mathlib/Data/Finsupp/AList.lean

@@ -76,17 +76,15 @@ noncomputable def lookupFinsupp (l : AList fun _x : α => M) : α →₀ M
 @[simp]
 theorem lookupFinsupp_apply [DecidableEq α] (l : AList fun _x : α => M) (a : α) :
     l.lookupFinsupp a = (l.lookup a).getD 0 := by
-    -- porting note: was `convert rfl`
-    simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]; congr
+    convert rfl; congr
 #align alist.lookup_finsupp_apply AList.lookupFinsupp_apply
 
 @[simp]
 theorem lookupFinsupp_support [DecidableEq α] [DecidableEq M] (l : AList fun _x : α => M) :
     l.lookupFinsupp.support = (l.1.filter fun x => Sigma.snd x ≠ 0).keys.toFinset := by
-    -- porting note: was `convert rfl`
-     simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]; congr
-     · apply Subsingleton.elim
-     · funext; congr
+  convert rfl; congr
+  · apply Subsingleton.elim
+  · funext; congr
 #align alist.lookup_finsupp_support AList.lookupFinsupp_support
 
 theorem lookupFinsupp_eq_iff_of_ne_zero [DecidableEq α] {l : AList fun _x : α => M} {a : α} {x : M}

Mathlib/Logic/Hydra.lean

@@ -110,10 +110,7 @@ theorem cutExpand_fibration (r : α → α → Prop) :
     Fibration (GameAdd (CutExpand r) (CutExpand r)) (CutExpand r) fun s ↦ s.1 + s.2 := by
   rintro ⟨s₁, s₂⟩ s ⟨t, a, hr, he⟩; dsimp at he ⊢
   classical
-  -- Porting note: Originally `obtain ⟨ha, rfl⟩`
-  -- This is https://github.com/leanprover/std4/issues/62
-  obtain ⟨ha, hb⟩ := add_singleton_eq_iff.1 he
-  rw [hb]
+  obtain ⟨ha, rfl⟩ := add_singleton_eq_iff.1 he
   rw [add_assoc, mem_add] at ha
   obtain h | h := ha
   · refine' ⟨(s₁.erase a + t, s₂), GameAdd.fst ⟨t, a, hr, _⟩, _⟩

Mathlib/RingTheory/WittVector/Isocrystal.lean

@@ -197,11 +197,7 @@ instance (m : ℤ) : Isocrystal p k (StandardOneDimIsocrystal p k m) where
 
 @[simp]
 theorem StandardOneDimIsocrystal.frobenius_apply (m : ℤ) (x : StandardOneDimIsocrystal p k m) :
-    Φ(p, k) x = (p : K(p, k)) ^ m • φ(p, k) x := by
-  -- Porting note: was just `rfl`
-  erw [smul_eq_mul]
-  simp only [map_zpow₀, map_natCast]
-  rfl
+    Φ(p, k) x = (p : K(p, k)) ^ m • φ(p, k) x := rfl
 #align witt_vector.standard_one_dim_isocrystal.frobenius_apply WittVector.StandardOneDimIsocrystal.frobenius_apply
 
 end PerfectRing