chore(Partition): tinygolf

leanprover-community · Apr 17, 2024 · fb10b9a · fb10b9a
1 parent 57b10af
commit fb10b9a
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/SphereEversion/ToMathlib/Partition.lean b/SphereEversion/ToMathlib/Partition.lean
@@ -53,8 +53,7 @@ theorem germ_combine_mem (φ : ι → M → F) (hx : x ∈ interior s := by simp
   rw [this]
   refine sum_mem_reallyConvexHull ?_ (ρ.sum_germ hx) (fun i hi ↦ mem_image_of_mem _ hi)
   · intro i _
-    filter_upwards
-    apply ρ.nonneg
+    filter_upwards using fun a ↦ ρ.nonneg i a
 
 end SmoothPartitionOfUnity