chore: avoid subst by rfl (#8145)

Co-authored-by: Moritz Firsching <firsching@google.com>
leanprover-community · Nov 3, 2023 · c539f36 · c539f36
1 parent b7a9938
commit c539f36
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/Mathlib/Analysis/BoundedVariation.lean b/Mathlib/Analysis/BoundedVariation.lean
@@ -861,9 +861,8 @@ namespace LocallyBoundedVariationOn
 `ae_differentiableWithinAt_of_mem`. -/
 theorem ae_differentiableWithinAt_of_mem_real {f : ℝ → ℝ} {s : Set ℝ}
     (h : LocallyBoundedVariationOn f s) : ∀ᵐ x, x ∈ s → DifferentiableWithinAt ℝ f s x := by
-  obtain ⟨p, q, hp, hq, fpq⟩ : ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q :=
+  obtain ⟨p, q, hp, hq, rfl⟩ : ∃ p q, MonotoneOn p s ∧ MonotoneOn q s ∧ f = p - q :=
     h.exists_monotoneOn_sub_monotoneOn
-  subst f -- porting note: TODO: `rfl` instead of `fpq` doesn't work
   filter_upwards [hp.ae_differentiableWithinAt_of_mem, hq.ae_differentiableWithinAt_of_mem] with
     x hxp hxq xs
   exact (hxp xs).sub (hxq xs)

diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean
@@ -1197,10 +1197,9 @@ theorem perm_of_mem_permutationsAux :
   refine' permutationsAux.rec (by simp) _
   introv IH1 IH2 m
   rw [permutationsAux_cons, permutations, mem_foldr_permutationsAux2] at m
-  rcases m with (m | ⟨l₁, l₂, m, _, e⟩)
+  rcases m with (m | ⟨l₁, l₂, m, _, rfl⟩)
   · exact (IH1 _ m).trans perm_middle
-  · subst e
-    have p : l₁ ++ l₂ ~ is := by
+  · have p : l₁ ++ l₂ ~ is := by
       simp [permutations] at m
       cases' m with e m
       · simp [e]