golfs

Mathlib/Data/Finset/Sym.lean

@@ -56,7 +56,7 @@ theorem mem_sym2_iff {m : Sym2 α} : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s := by
 theorem sym2_cons (a : α) (s : Finset α) (ha : a ∉ s) :
     (s.cons a ha).sym2 = ((s.cons a ha).map <| Sym2.mkEmbedding a).disjUnion s.sym2 (by
       simp [Finset.disjoint_left, ha]) :=
-  Finset.val_injective <| Multiset.sym2_cons _ _
+  val_injective <| Multiset.sym2_cons _ _
 
 theorem sym2_insert [DecidableEq α] (a : α) (s : Finset α) :
     (insert a s).sym2 = ((insert a s).image fun b => s(a, b)) ∪ s.sym2 := by
@@ -66,11 +66,11 @@ theorem sym2_insert [DecidableEq α] (a : α) (s : Finset α) :
   · simpa [map_eq_image] using sym2_cons a s ha
 
 theorem sym2_map (f : α ↪ β) (s : Finset α) : (s.map f).sym2 = s.sym2.map (.sym2Map f) :=
-  Finset.val_injective <| s.val.sym2_map _
+  val_injective <| s.val.sym2_map _
 
 theorem sym2_image [DecidableEq β] (f : α → β) (s : Finset α) :
     (s.image f).sym2 = s.sym2.image (Sym2.map f) := by
-  apply Finset.val_injective
+  apply val_injective
   dsimp [Finset.sym2]
   rw [← Multiset.dedup_sym2, Multiset.sym2_map]
 

Mathlib/Data/List/Sym.lean

@@ -126,11 +126,11 @@ theorem map_mk_sublist_sym2 (x : α) (xs : List α) (h : x ∈ xs) :
     simp [List.sym2]
     cases h with
     | head =>
-      exact Sublist.cons₂ _ (sublist_append_left _ _)
+      exact (sublist_append_left _ _).cons₂ _
     | tail _ h =>
-      apply Sublist.cons
+      refine .cons _ ?_
       rw [← singleton_append]
-      refine Sublist.append ?_ (ih h)
+      refine .append ?_ (ih h)
       rw [singleton_sublist, mem_map]
       exact ⟨_, h, Sym2.eq_swap⟩
 
@@ -142,7 +142,7 @@ theorem map_mk_disjoint_sym2 (x : α) (xs : List α) (h : x ∉ xs) :
     simp only [mem_cons, not_or] at h
     rw [List.sym2, map_cons, map_cons, disjoint_cons_left, disjoint_append_right,
       disjoint_cons_right]
-    refine ⟨?_, ⟨⟨?_, ?_⟩, ?_⟩⟩
+    refine ⟨?_, ⟨?_, ?_⟩, ?_⟩
     · refine not_mem_cons_of_ne_of_not_mem ?_ (not_mem_append ?_ ?_)
       · simp [h.1]
       · simp_rw [mem_map, not_exists, not_and]