chore(AlgebraicTopology/TopologicalSimplex): clean up, golf (#9431)

Mathlib/AlgebraicTopology/TopologicalSimplex.lean

@@ -17,26 +17,23 @@ topological `n`-simplex.
 This is used to define `TopCat.toSSet` in `AlgebraicTopology.SingularSet`.
 -/
 
+set_option linter.uppercaseLean3 false
 
 noncomputable section
 
 namespace SimplexCategory
 
 open Simplicial NNReal BigOperators Classical CategoryTheory
 
-attribute [local instance]
-  CategoryTheory.ConcreteCategory.hasCoeToSort CategoryTheory.ConcreteCategory.funLike
+attribute [local instance] ConcreteCategory.hasCoeToSort ConcreteCategory.funLike
 
 -- porting note: added, should be moved
-instance (x : SimplexCategory) : Fintype (CategoryTheory.ConcreteCategory.forget.obj x) := by
-  change (Fintype (Fin _))
-  infer_instance
+instance (x : SimplexCategory) : Fintype (ConcreteCategory.forget.obj x) :=
+  inferInstanceAs (Fintype (Fin _))
 
 /-- The topological simplex associated to `x : SimplexCategory`.
   This is the object part of the functor `SimplexCategory.toTop`. -/
-def toTopObj (x : SimplexCategory) :=
-  { f : x → ℝ≥0 | ∑ i, f i = 1 }
-set_option linter.uppercaseLean3 false in
+def toTopObj (x : SimplexCategory) := { f : x → ℝ≥0 | ∑ i, f i = 1 }
 #align simplex_category.to_Top_obj SimplexCategory.toTopObj
 
 instance (x : SimplexCategory) : CoeFun x.toTopObj fun _ => x → ℝ≥0 :=
@@ -45,43 +42,30 @@ instance (x : SimplexCategory) : CoeFun x.toTopObj fun _ => x → ℝ≥0 :=
 @[ext]
 theorem toTopObj.ext {x : SimplexCategory} (f g : x.toTopObj) : (f : x → ℝ≥0) = g → f = g :=
   Subtype.ext
-set_option linter.uppercaseLean3 false in
 #align simplex_category.to_Top_obj.ext SimplexCategory.toTopObj.ext
 
 /-- A morphism in `SimplexCategory` induces a map on the associated topological spaces. -/
-def toTopMap {x y : SimplexCategory} (f : x ⟶ y) : x.toTopObj → y.toTopObj := fun g =>
-  ⟨fun i => ∑ j in Finset.univ.filter fun k => f k = i, g j, by
-    simp only [Finset.sum_congr, toTopObj, Set.mem_setOf]
+def toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) : y.toTopObj :=
+  ⟨fun i => ∑ j in Finset.univ.filter (f · = i), g j, by
+    simp only [toTopObj, Set.mem_setOf]
     rw [← Finset.sum_biUnion]
-    have hg := g.2
-    dsimp [toTopObj] at hg
-    convert hg
-    · simp [Finset.eq_univ_iff_forall]
-    · intro i _ j _ h
-      rw [Function.onFun, disjoint_iff_inf_le]
-      intro e he
-      simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
-      apply h
-      simp only [Finset.mem_univ, forall_true_left,
-        ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
-        Finset.mem_filter, true_and] at he
-      rw [← he.1, he.2]⟩
-set_option linter.uppercaseLean3 false in
+    · have hg : ∑ i : (forget SimplexCategory).obj x, g i = 1 := g.2
+      convert hg
+      simp [Finset.eq_univ_iff_forall]
+    · apply Set.pairwiseDisjoint_filter⟩
 #align simplex_category.to_Top_map SimplexCategory.toTopMap
 
 @[simp]
 theorem coe_toTopMap {x y : SimplexCategory} (f : x ⟶ y) (g : x.toTopObj) (i : y) :
-    toTopMap f g i = ∑ j in Finset.univ.filter fun k => f k = i, g j :=
+    toTopMap f g i = ∑ j in Finset.univ.filter (f · = i), g j :=
   rfl
-set_option linter.uppercaseLean3 false in
 #align simplex_category.coe_to_Top_map SimplexCategory.coe_toTopMap
 
 @[continuity]
 theorem continuous_toTopMap {x y : SimplexCategory} (f : x ⟶ y) : Continuous (toTopMap f) := by
   refine' Continuous.subtype_mk (continuous_pi fun i => _) _
   dsimp only [coe_toTopMap]
   exact continuous_finset_sum _ (fun j _ => (continuous_apply _).comp continuous_subtype_val)
-set_option linter.uppercaseLean3 false in
 #align simplex_category.continuous_to_Top_map SimplexCategory.continuous_toTopMap
 
 /-- The functor associating the topological `n`-simplex to `[n] : SimplexCategory`. -/
@@ -94,7 +78,7 @@ def toTop : SimplexCategory ⥤ TopCat where
     ext f
     apply toTopObj.ext
     funext i
-    change (Finset.univ.filter fun k => k = i).sum _ = _
+    change (Finset.univ.filter (· = i)).sum _ = _
     simp [Finset.sum_filter, CategoryTheory.id_apply]
   map_comp := fun f g => by
     ext h
@@ -109,16 +93,7 @@ def toTop : SimplexCategory ⥤ TopCat where
     · apply Finset.sum_congr
       · exact Finset.ext (fun j => ⟨fun hj => by simpa using hj, fun hj => by simpa using hj⟩)
       · tauto
-    · intro j _ k _ h
-      rw [Function.onFun, disjoint_iff_inf_le]
-      intro e he
-      simp only [Finset.bot_eq_empty, Finset.not_mem_empty]
-      apply h
-      simp only [Finset.mem_univ, forall_true_left,
-        ge_iff_le, Finset.le_eq_subset, Finset.inf_eq_inter, Finset.mem_inter,
-        Finset.mem_filter, true_and] at he
-      rw [← he.1, he.2]
-set_option linter.uppercaseLean3 false in
+    · apply Set.pairwiseDisjoint_filter
 #align simplex_category.to_Top SimplexCategory.toTop
 
 -- These lemmas have always been bad (#7657), but leanprover/lean4#2644 made `simp` start noticing

Mathlib/Data/Finset/Basic.lean

@@ -2917,6 +2917,13 @@ theorem filter_disj_union (s : Finset α) (t : Finset α) (h : Disjoint s t) :
   eq_of_veq <| Multiset.filter_add _ _ _
 #align finset.filter_disj_union Finset.filter_disj_union
 
+lemma _root_.Set.pairwiseDisjoint_filter [DecidableEq β] (f : α → β) (s : Set β) (t : Finset α) :
+    s.PairwiseDisjoint fun x ↦ t.filter (f · = x) := by
+  rintro i - j - h u hi hj x hx
+  obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx
+  obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx
+  contradiction
+
 theorem filter_cons {a : α} (s : Finset α) (ha : a ∉ s) :
     filter p (cons a s ha) =
       (if p a then {a} else ∅ : Finset α).disjUnion (filter p s)