chore: backport some simpler proofs from lean-pr-testing-6053 (#19176)

A few things that break under leanprover/lean4#6053 admit nicer proofs anyway, so backport these more robust proofs.
leanprover-community · Nov 18, 2024 · d51f67b · d51f67b
1 parent a2d097b
commit d51f67b
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 8 deletions.
diff --git a/Mathlib/CategoryTheory/Quotient.lean b/Mathlib/CategoryTheory/Quotient.lean
@@ -174,7 +174,7 @@ theorem lift_unique (Φ : Quotient r ⥤ D) (hΦ : functor r ⋙ Φ = F) : Φ =
   · rintro _ _ f
     dsimp [lift, Functor]
     refine Quot.inductionOn f (fun _ ↦ ?_) -- Porting note: this line was originally an `apply`
-    simp only [Quot.liftOn_mk, Functor.comp_map]
+    simp only [heq_eq_eq]
     congr
 
 lemma lift_unique' (F₁ F₂ : Quotient r ⥤ D) (h : functor r ⋙ F₁ = functor r ⋙ F₂) :

diff --git a/Mathlib/Data/List/Cycle.lean b/Mathlib/Data/List/Cycle.lean
@@ -825,10 +825,7 @@ theorem chain_map {β : Type*} {r : α → α → Prop} (f : β → α) {s : Cyc
   Quotient.inductionOn s fun l => by
     cases' l with a l
     · rfl
-    dsimp only [Chain, Quotient.liftOn_mk, Cycle.map, Quotient.map', Quot.map,
-      Quotient.liftOn', Quotient.liftOn, Quot.liftOn_mk, List.map]
-    rw [← concat_eq_append, ← List.map_concat, List.chain_map f]
-    simp
+    · simp [← concat_eq_append, ← List.map_concat, List.chain_map f]
 
 nonrec theorem chain_range_succ (r : ℕ → ℕ → Prop) (n : ℕ) :
     Chain r (List.range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ := by

diff --git a/Mathlib/Data/TypeVec.lean b/Mathlib/Data/TypeVec.lean
@@ -604,9 +604,7 @@ theorem dropFun_of_subtype {α} (p : α ⟹ «repeat» (n + 1) Prop) :
 
 @[simp]
 theorem lastFun_of_subtype {α} (p : α ⟹ «repeat» (n + 1) Prop) :
-    lastFun (ofSubtype p) = _root_.id := by
-  ext i : 2
-  induction i; simp [dropFun, *]; rfl
+    lastFun (ofSubtype p) = _root_.id := rfl
 
 @[simp]
 theorem dropFun_RelLast' {α : TypeVec n} {β} (R : β → β → Prop) :