diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5c7f246c14..e77eb7dc39 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -12,6 +12,9 @@
 
 ### Changed
 
+- in `mathcomp_extra.v`
+  + lemmas `eq_bigmax`, `eq_bigmin` changed to respect `P` in the returned type.
+
 ### Renamed
 
 - in `lebesgue_measure.v`:
diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v
index b78ae58f45..10c031ecb7 100644
--- a/classical/mathcomp_extra.v
+++ b/classical/mathcomp_extra.v
@@ -830,8 +830,10 @@ by apply/bigmax_leP; split => //; exact: PxF.
 Qed.
 
 Lemma eq_bigmax j P F : P j -> (forall i, P i -> x <= F i) ->
-  {i0 | i0 \in I & \big[max/x]_(i | P i) F i = F i0}.
-Proof. by move=> Pi0 Hx; rewrite (bigmax_eq_arg Pi0) //; eexists. Qed.
+  {i0 | i0 \in P & \big[max/x]_(i | P i) F i = F i0}.
+Proof.
+by move=> Pi0 Hx; rewrite (bigmax_eq_arg Pi0) //; eexists => //; case:arg_maxP.
+Qed.
 
 Lemma le_bigmax2 P F1 F2 : (forall i, P i -> F1 i <= F2 i) ->
   \big[max/x]_(i | P i) F1 i <= \big[max/x]_(i | P i) F2 i.
@@ -980,8 +982,10 @@ by apply/bigmin_geP; split => //; exact: PFx.
 Qed.
 
 Lemma eq_bigmin j P F : P j -> (forall i, P i -> F i <= x) ->
-  {i0 | i0 \in I & \big[min/x]_(i | P i) F i = F i0}.
-Proof. by move=> Pi0 Hx; rewrite (bigmin_eq_arg Pi0) //; eexists. Qed.
+  {i0 | i0 \in P & \big[min/x]_(i | P i) F i = F i0}.
+Proof.
+by move=> Pi0 Hx; rewrite (bigmin_eq_arg Pi0) //; eexists => //; case:arg_minP.
+Qed.
 
 End bigmin_finType.